Theorems · Theorem · combinatorics
SimpleGraph.ComponentCompl.hom_trans
∀ {V : Type u} {G : SimpleGraph V} {K L M : Set V} (C : G.ComponentCompl L) (h : K ⊆ L) (h' : M ⊆ K),
SimpleGraph.ComponentCompl.hom ⋯ C = SimpleGraph.ComponentCompl.hom h' (SimpleGraph.ComponentCompl.hom h C)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- LE.le.transstatement and proof · cited by 3,151
- SimpleGraphstatement and proof · cited by 3,072
- Compl.complproof · cited by 2,925
- SimpleGraph.Homproof · cited by 139
- SimpleGraph.ConnectedComponentproof · cited by 86
- SimpleGraph.induceproof · cited by 80
- SimpleGraph.ComponentComplstatement and proof · cited by 29
- SimpleGraph.ComponentCompl.homstatement · cited by 12
- SimpleGraph.Hom.idproof · cited by 11
- SimpleGraph.ConnectedComponent.mapproof · cited by 11
- SimpleGraph.induceHomproof · cited by 7
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.