Properties

Statistics

Metric	Count
Definitions	0
Theorems `componentComplFunctor_finite`, `componentComplFunctor_nonempty_of_infinite`, `end_componentCompl_infinite`, `instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite`, `nonempty_ends_of_infinite`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`componentComplFunctor_finite` 📖	mathematical	—	`Finite` `CategoryTheory.Functor.obj` `Opposite` `Finset` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `CategoryTheory.types` `componentComplFunctor`	—	`componentCompl_finite`
`componentComplFunctor_nonempty_of_infinite` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `Finset` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `CategoryTheory.types` `componentComplFunctor`	—	`componentCompl_nonempty_of_infinite`
`end_componentCompl_infinite` 📖	mathematical	—	`Set.Infinite` `ComponentCompl.supp` `SetLike.coe` `Finset` `Finset.instSetLike` `Opposite.unop` `Set` `Set.instMembership` `end`	—	`ComponentCompl.infinite_iff_in_all_ranges` `Subtype.prop`
`instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite` 📖	mathematical	—	`IsEmpty` `Set.Elem` `end`	—	`nonempty_fintype` `ComponentCompl.nonempty` `Set.disjoint_iff` `ComponentCompl.disjoint_right` `Finset.coe_univ`
`nonempty_ends_of_infinite` 📖	mathematical	—	`Set.Nonempty` `end`	—	`nonempty_sections_of_finite_inverse_system` `Finset.isDirected_le` `componentComplFunctor_finite` `componentComplFunctor_nonempty_of_infinite`

---