Conversation
There was a problem hiding this comment.
I've left some suggestions up until induce_walk_support_connected.
In general, I think we need these results to be generalized to apply to subgraphs, where they're more naturally stated. We also need a bit more development on simple_graph.walk.to_subgraph.
Note that for the code I wrote I didn't think too hard about naming or implicit/explicit arguments.
|
I started a rewrite according to your input @kmill:
Is that looking better? |
|
OK, I've cleaned things up a bit, but since I actually don't need the lemma subgraph.sUnion_connected_of_pairwise_not_disjoint {S : set G.subgraph} (Sn : S.nonempty)
(Snd : ∀ {s : G.subgraph}, s ∈ S → ∀ {t : G.subgraph}, t ∈ S → (s ⊓ t).verts.nonempty)
(Sc : ∀ {s : G.subgraph}, s ∈ S → s.connected) :
(⨆ (s ∈ S), s).connected := sorry
OK I've removed the "complete_lattice" definitions and the |
| import combinatorics.simple_graph.connectivity | ||
| import combinatorics.simple_graph.subgraph | ||
| /-! | ||
| # Connectivity of subgraphs |
There was a problem hiding this comment.
| # Connectivity of subgraphs | |
| # Connectivity of subgraphs and induced graphs |
Could you also move everything that's specifically about induced graphs (not induced subgraphs) to a section at the end?
It would also be good to arrange other things more thematically, like putting walk.to_subgraph_connected right after its two supporting lemmas.
There was a problem hiding this comment.
It would also be good to arrange other things more thematically, like putting
walk.to_subgraph_connectedright after its two supporting lemmas.
Not sure exactly how to do that, since walk.to_subgraph_connected the dependencies of lemmas aren't really linear starting with .sup, but I tried.
…ivity/connectivity_of_induced_graphs
|
This is now replaced by a mathlib4 PR: leanprover-community/mathlib4#5927 |
(Replaces [mathlib#18454](leanprover-community/mathlib3#18454).) Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
(Replaces [mathlib#18454](leanprover-community/mathlib3#18454).) Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
(Replaces [mathlib#18454](leanprover-community/mathlib3#18454).) Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
(Replaces [mathlib#18454](leanprover-community/mathlib3#18454).) Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
(Replaces [mathlib#18454](leanprover-community/mathlib3#18454).) Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
Co-authored-by: Kyle Miller kmill31415@gmail.com