Theorems · Theorem · combinatorics
SimpleGraph.connected_induce_iff
∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, (SimpleGraph.induce s G).Connected ↔ (⊤.induce s).Connected- Cited by
- 4 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.Connectedstatement and proof · cited by 75
- SimpleGraph.Subgraph.inducestatement and proof · cited by 33
- SimpleGraph.Subgraph.Connectedstatement and proof · cited by 24
- SimpleGraph.induce_eq_coe_induce_topproof · cited by 4
- SimpleGraph.Subgraph.connected_iff'proof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- SimpleGraph.Subgraph.Connected.induce_vertsproof · cited by 1
- SimpleGraph.induce_union_connectedproof · cited by 1
- SimpleGraph.induce_pair_connected_of_adjproof · cited by 0
- SimpleGraph.connected_induce_unionproof · cited by 0