Theorems · Theorem · combinatorics
SimpleGraph.preconnected_induce_iff
∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, (SimpleGraph.induce s G).Preconnected ↔ (⊤.induce s).Preconnected- Cited by
- 2 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Top.topstatement and proof · cited by 9,680
- Set.Elemstatement and proof · cited by 7,166
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Subgraphstatement · cited by 326
- SimpleGraph.inducestatement · cited by 80
- SimpleGraph.Preconnectedstatement and proof · cited by 49
- SimpleGraph.Subgraph.inducestatement and proof · cited by 33
- SimpleGraph.Subgraph.Preconnectedstatement and proof · cited by 14
- SimpleGraph.Subgraph.preconnected_iffproof · cited by 5
- SimpleGraph.induce_eq_coe_induce_topproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- SimpleGraph.induce_union_connectedproof · cited by 1
- SimpleGraph.connected_induce_unionproof · cited by 0