Documentation Verification Report

Finite

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems `finite`, `finite_iSup_iff`, `finite_iff_of_iso`, `finite_of_epi`, `finite_of_hasDimensionLT`, `finite_of_iso`, `finite_of_mono`, `finite_range`, `finite_subcomplex_top_iff`, `hasDimensionLT_of_finite`, `instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite`, `instFiniteObjOppositeSimplexCategoryOfFinite`, `instFiniteToSSet`	13
Total	13

SSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iSup_iff` 📖	mathematical	—	`Finite` `Subcomplex.toSSet` `iSup` `Subcomplex` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory`	—	`finite_of_mono` `le_iSup` `Subcomplex.mono_homOfLE` `Finite.of_surjective` `Finite.instSigma` `Finite.finite` `N.nonDegenerate` `Subtype.prop` `N.mk_surjective` `CategoryTheory.Subfunctor.iSup_obj` `Subcomplex.mem_nonDegenerate_iff`
`finite_iff_of_iso` 📖	mathematical	—	`Finite`	—	`finite_of_iso`
`finite_of_epi` 📖	mathematical	—	`Finite`	—	`hasDimensionLT_of_finite` `hasDimensionLT_of_epi` `finite_of_hasDimensionLT` `Finite.of_surjective` `instFiniteObjOppositeSimplexCategoryOfFinite` `CategoryTheory.NatTrans.epi_iff_epi_app` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `Subtype.finite`
`finite_of_hasDimensionLT` 📖	mathematical	`Finite` `Set.Elem` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `nonDegenerate`	`Finite`	—	`Finite.of_surjective` `Finite.instSigma` `Finite.of_fintype` `N.nonDegenerate` `nonDegenerate_eq_bot_of_hasDimensionLT`
`finite_of_iso` 📖	mathematical	—	`Finite`	—	`finite_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_inv`
`finite_of_mono` 📖	mathematical	—	`Finite`	—	`hasDimensionLT_of_finite` `hasDimensionLT_of_mono` `finite_of_hasDimensionLT` `Finite.of_injective` `instFiniteObjOppositeSimplexCategoryOfFinite` `CategoryTheory.injective_of_mono` `CategoryTheory.instMonoAppOfFunctor` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `Subtype.val_injective`
`finite_range` 📖	mathematical	—	`Finite` `Subcomplex.toSSet` `Subcomplex.range`	—	`finite_of_epi` `Subcomplex.instEpiToRange`
`finite_subcomplex_top_iff` 📖	mathematical	—	`Finite` `Subcomplex.toSSet` `Top.top` `Subcomplex` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`finite_iff_of_iso`
`hasDimensionLT_of_finite` 📖	mathematical	—	`HasDimensionLT`	—	`Finite.finite` `Finset.max_of_nonempty` `Finset.not_nonempty_iff_eq_empty` `Nat.instCanonicallyOrderedAdd` `Set.ext`
`instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite` 📖	mathematical	—	`Finite` `Set.Elem` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `nonDegenerate`	—	`Finite.of_injective` `Finite.finite` `S.ext_iff'` `N.ext_iff`
`instFiniteObjOppositeSimplexCategoryOfFinite` 📖	mathematical	—	`Finite` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types`	—	`exists_nonDegenerate` `SimplexCategory.le_of_epi` `Finite.of_surjective` `Finite.instSigma` `Finite.of_fintype` `SimplexCategory.instFiniteHom` `instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite`
`instFiniteToSSet` 📖	mathematical	—	`Finite` `Subcomplex.toSSet`	—	`hasDimensionLT_of_finite` `finite_of_hasDimensionLT` `Subcomplex.instHasDimensionLTToSSet` `Finite.of_injective` `instFiniteObjOppositeSimplexCategoryOfFinite`

SSet.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite` `SSet.N`	—	—

---

← Back to Index