feat(Combinatorics/SimpleGraph/Acyclic): add delete leaf from tree gives tree#36850
feat(Combinatorics/SimpleGraph/Acyclic): add delete leaf from tree gives tree#36850whocares-abt wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
stating that we get a tree if removing a leaf from tree
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. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. 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. |
PR summary cf61572730Import 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
|
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
whocares-abt
changed the title
|
|
||
| /-- Removing a leaf from a tree gives another tree. -/ | ||
| lemma IsTree.tree_if_removed_leaf (v : V) [Fintype ↑(G.neighborSet v)] | ||
| (h1 : G.IsTree) (h2 : G.degree v = 1) : (G.induce {v}ᶜ).IsTree := by |
There was a problem hiding this comment.
Use h\1 (subscript) instead of h1. Also spacing to match mathlib style.
| (h1 : G.IsTree) (h2 : G.degree v = 1) : (G.induce {v}ᶜ).IsTree := by | |
| (h₁ : G.IsTree) (h₂ : G.degree v = 1) : (G.induce {v}ᶜ).IsTree := by |
| constructor | ||
| · exact (Connected.induce_compl_singleton_of_degree_eq_one h1.isConnected) h2 | ||
| · exact IsAcyclic.induce h1.IsAcyclic {v}ᶜ |
There was a problem hiding this comment.
I would just have this be a term-mode proof. Note that you can significantly shortern it by using dot notation when it's available. (I also changed the name isConnected -> connected IsAcylic -> isAcyclic since Yael just landed a change updating the names.)
| constructor | |
| · exact (Connected.induce_compl_singleton_of_degree_eq_one h1.isConnected) h2 | |
| · exact IsAcyclic.induce h1.IsAcyclic {v}ᶜ | |
| ⟨h₁.connected.induce_compl_singleton_of_degree_eq_one h₂, h₁.isAcyclic.induce {v}ᶜ⟩ |
| exact ⟨v, hv.preconnected⟩ | ||
|
|
||
| /-- Removing a leaf from a tree gives another tree. -/ | ||
| lemma IsTree.tree_if_removed_leaf (v : V) [Fintype ↑(G.neighborSet v)] |
There was a problem hiding this comment.
This name doesn't match mathlib's naming convention https://leanprover-community.github.io/contribute/naming.html
I am not expert in this domain, but I would probably use IsTree.induce_compl_singleton_of_degree_eq_one to match the Connected version.
vlad902
left a comment
vlad902
left a comment
There was a problem hiding this comment.
Once you've addressed review comments, you should mark them resolved on GitHub so the next reviewer knows they are no longer relevant.
Co-authored-by: Vlad Tsyrklevich <[email protected]>
2 participants
Added theorem stating Deleting a leaf from a tree produces a tree.