Theorems · Definition · combinatorics
SimpleGraph.componentComplFunctor
{V : Type u} → SimpleGraph V → CategoryTheory.Functor (Finset V)ᵒᵖ (Type u)The functor assigning, to a finite set in V, the set of connected components in its complement.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- Finsetstatement and proof · cited by 13,712
- SetLike.coeproof · cited by 8,199
- Oppositestatement and proof · cited by 8,081
- SimpleGraphstatement and proof · cited by 3,072
- Opposite.unopproof · cited by 2,231
- TypeCat.ofHomproof · cited by 389
- SimpleGraph.ComponentComplproof · cited by 29
- SimpleGraph.ComponentCompl.homproof · cited by 12
Cited by7
Results whose statement or proof uses this declaration.
- SimpleGraph.endstatement and proof · cited by 3
- SimpleGraph.componentComplFunctor_mapstatement and proof · cited by 1
- SimpleGraph.infinite_iff_in_eventualRangestatement and proof · cited by 0
- SimpleGraph.nonempty_ends_of_infinitestatement and proof · cited by 0
- SimpleGraph.end_componentCompl_infinitestatement · cited by 0
- SimpleGraph.end_hom_mk_of_mkstatement and proof · cited by 0
- SimpleGraph.componentComplFunctor_objstatement and proof · cited by 0