feat(SimpleGraph): redefine IsBridge via deleteEdges#36022
feat(SimpleGraph): redefine IsBridge via deleteEdges#36022SproutSeeds wants to merge 1 commit intoleanprover-community:masterfrom
IsBridge via deleteEdges#36022Conversation
- drop edge-membership requirement from IsBridge definition - adapt bridge lemmas to take adjacency/membership assumptions explicitly - update downstream proofs in EdgeConnectivity, Acyclic, Hamiltonian - verification: lake build
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
SproutSeeds
changed the title
IsBridge via deleteEdges
PR summary 6a736c34dfImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
Marked this PR ready for review. CI was green on the current branch when switching out of draft. |
|
Hello from triage: your PR description shares features with many AI-written texts --- did you use AI to create this PR? If so, please mention that and how you used AI in your PR description. This helps us review your PR better. Thanks! |
grunweg
added
the
awaiting-author
grunweg
added
the
LLM-generated
3 participants
Closes #31690
Redefines
SimpleGraph.IsBridgevia deletion-only connectivity, without embedding edge membership into the definition.Updates bridge definition and supporting lemmas.
Validation: targeted
lake buildandlake exe runLinter --tracepassed for touched module(s).Intelligent systems usage: tool=Codex; model=Codex 5.3; effort=extra high; workflow=ORP local-first gates (viability/overlap/naturality/targeted build+linter/draft CI); scope=drafting/refactoring/proof exploration including PR description drafting; final code choices and validation by me.
Happy to adjust naming, placement, or proof style based on maintainer preference.