Theorems · Theorem · combinatorics

SimpleGraph.induce_union_connected

∀ {V : Type u} {G : SimpleGraph V} {s t : Set V},
  (SimpleGraph.induce s G).Preconnected →
    (SimpleGraph.induce t G).Preconnected → (s ∩ t).Nonempty → (SimpleGraph.induce (s ∪ t) G).Connected

Defined in: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Cited by: 1 results in Mathlib
Foundations: Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.Elemstatement · cited by 7,166
SimpleGraphstatement and proof · cited by 3,072
Set.Nonemptystatement and proof · cited by 2,627
SimpleGraph.inducestatement and proof · cited by 80
SimpleGraph.Connectedstatement · cited by 75
SimpleGraph.Preconnectedstatement and proof · cited by 49
SimpleGraph.connected_induce_iffproof · cited by 4
SimpleGraph.preconnected_induce_iffproof · cited by 2
SimpleGraph.Subgraph.induce_union_connectedproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjointproof · cited by 0