Theorems · Inductive type · combinatorics
SimpleGraph.Connected
{V : Type u} → SimpleGraph V → PropA graph is connected if it's preconnected and contains at least one vertex.
This follows the convention observed by mathlib that something is connected iff it has
exactly one connected component.
There is a CoeFun instance so that h u v can be used instead of h.Preconnected u v.
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement · cited by 3,072
Cited by81
Results whose statement or proof uses this declaration.
- SimpleGraph.Connected.preconnectedstatement and proof · cited by 28
- SimpleGraph.IsTree.connectedstatement · cited by 9
- SimpleGraph.Connected.nonemptystatement and proof · cited by 9
- SimpleGraph.ConnectedComponent.connected_toSimpleGraphstatement · cited by 6
- SimpleGraph.connected_iffstatement and proof · cited by 6
- SimpleGraph.connected_iff_exists_forall_reachablestatement · cited by 6
- SimpleGraph.connected_induce_iffstatement and proof · cited by 4
- SimpleGraph.Connected.exists_isPathstatement and proof · cited by 4
- SimpleGraph.Subgraph.Connected.coestatement · cited by 4
- SimpleGraph.not_connected_botstatement · cited by 3
- SimpleGraph.Subgraph.connected_iff'statement and proof · cited by 3
- SimpleGraph.ediam_eq_top_of_not_connectedstatement and proof · cited by 3