Theorems · Theorem · combinatorics
SimpleGraph.ConnectedComponent.reachable_of_mem_supp
∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}, u ∈ C.supp → v ∈ C.supp → G.Reachable u v- Cited by
- 2 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Reachablestatement · cited by 141
- SimpleGraph.ConnectedComponentstatement and proof · cited by 86
- SimpleGraph.ConnectedComponent.suppstatement and proof · cited by 42
- SimpleGraph.ConnectedComponent.mem_supp_iffproof · cited by 4
- SimpleGraph.ConnectedComponent.exactproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- SimpleGraph.reachable_eq_of_maximal_isAcyclicproof · cited by 2
- SimpleGraph.ConnectedComponent.reachable_toSimpleGraphproof · cited by 1