Documentation Verification Report

Dimension

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

Statistics

Metric	Count
Definitions `HasDimensionLE`, `HasDimensionLT`	2
Theorems `degenerate_eq_top`, `eq_top_iff_of_hasDimensionLT`, `hasDimensionLT_of_le`, `instHasDimensionLTToSSet`, `le_iff_of_hasDimensionLT`, `degenerate_eq_top_of_hasDimensionLT`, `dim_le_of_nonDegenerate`, `dim_lt_of_nonDegenerate`, `hasDimensionLT_iSup_iff`, `hasDimensionLT_iff`, `hasDimensionLT_iff_of_iso`, `hasDimensionLT_of_epi`, `hasDimensionLT_of_le`, `hasDimensionLT_of_mono`, `hasDimensionLT_subcomplex_top_iff`, `instHasDimensionLTHAddNat`, `instHasDimensionLTToSSetBotSubcomplex`, `instHasDimensionLTToSSetRange`, `nonDegenerate_eq_bot_of_hasDimensionLT`	19
Total	21

SSet

Definitions

Name	Category	Theorems
`HasDimensionLE` 📖	MathDef	5 math math: `instHasDimensionLETensorUnitOfNatNat`, `prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat`, `instHasDimensionLETensorObjHAddNat`, `stdSimplex.instHasDimensionLEObjSimplexCategoryMk`, `hasDimensionLE_prod`
`HasDimensionLT` 📖	CompData	15 math math: `instHasDimensionLTToSSetRange`, `hasDimensionLT_of_epi`, `hasDimensionLT_prod`, `Subcomplex.hasDimensionLT_of_le`, `Subcomplex.instHasDimensionLTToSSet`, `hasDimensionLT_subcomplex_top_iff`, `hasDimensionLT_iff`, `instHasDimensionLTToSSetBotSubcomplex`, `hasDimensionLT_of_finite`, `hasDimensionLT_of_le`, `instHasDimensionLTTensorObjHAddNat`, `instHasDimensionLTHAddNat`, `hasDimensionLT_iSup_iff`, `hasDimensionLT_iff_of_iso`, `hasDimensionLT_of_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degenerate_eq_top_of_hasDimensionLT` 📖	mathematical	—	`degenerate` `Top.top` `Set` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`HasDimensionLT.degenerate_eq_top`
`dim_le_of_nonDegenerate` 📖	—	—	—	—	`dim_lt_of_nonDegenerate`
`dim_lt_of_nonDegenerate` 📖	—	—	—	—	`nonDegenerate_eq_bot_of_hasDimensionLT`
`hasDimensionLT_iSup_iff` 📖	mathematical	—	`HasDimensionLT` `Subcomplex.toSSet` `iSup` `Subcomplex` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory`	—	`CategoryTheory.Subfunctor.iSup_obj`
`hasDimensionLT_iff` 📖	mathematical	—	`HasDimensionLT` `degenerate` `Top.top` `Set` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	—
`hasDimensionLT_iff_of_iso` 📖	mathematical	—	`HasDimensionLT`	—	`hasDimensionLT_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv`
`hasDimensionLT_of_epi` 📖	mathematical	—	`HasDimensionLT`	—	`Set.ext` `CategoryTheory.epi_iff_surjective` `CategoryTheory.instEpiAppOfFunctor` `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` `degenerate_app_apply` `degenerate_eq_top_of_hasDimensionLT`
`hasDimensionLT_of_le` 📖	mathematical	—	`HasDimensionLT`	—	`degenerate_eq_top_of_hasDimensionLT` `LE.le.trans`
`hasDimensionLT_of_mono` 📖	mathematical	—	`HasDimensionLT`	—	`Set.ext` `degenerate_iff_of_isIso` `Subcomplex.instIsIsoToRangeOfMono` `Subcomplex.mem_degenerate_iff` `degenerate_eq_top_of_hasDimensionLT`
`hasDimensionLT_subcomplex_top_iff` 📖	mathematical	—	`HasDimensionLT` `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`	—	`hasDimensionLT_iff_of_iso`
`instHasDimensionLTHAddNat` 📖	mathematical	—	`HasDimensionLT`	—	`hasDimensionLT_of_le`
`instHasDimensionLTToSSetBotSubcomplex` 📖	mathematical	—	`HasDimensionLT` `Subcomplex.toSSet` `Bot.bot` `Subcomplex` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Set.ext`
`instHasDimensionLTToSSetRange` 📖	mathematical	—	`HasDimensionLT` `Subcomplex.toSSet` `Subcomplex.range`	—	`hasDimensionLT_of_epi` `Subcomplex.instEpiToRange`
`nonDegenerate_eq_bot_of_hasDimensionLT` 📖	mathematical	—	`nonDegenerate` `Bot.bot` `Set` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `BooleanAlgebra.toBot` `Set.instBooleanAlgebra`	—	`degenerate_eq_top_of_hasDimensionLT` `Set.compl_univ`

SSet.HasDimensionLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degenerate_eq_top` 📖	mathematical	—	`SSet.degenerate` `Top.top` `Set` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	—

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_iff_of_hasDimensionLT` 📖	mathematical	—	`Top.top` `SSet.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` `Set` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Opposite.op` `Set.instHasSubset` `SSet.nonDegenerate` `CategoryTheory.Subfunctor.obj`	—	`le_iff_of_hasDimensionLT` `Set.univ_inter`
`hasDimensionLT_of_le` 📖	mathematical	`SSet.Subcomplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory`	`SSet.HasDimensionLT` `toSSet`	—	`SSet.hasDimensionLT_of_mono` `mono_homOfLE`
`instHasDimensionLTToSSet` 📖	mathematical	—	`SSet.HasDimensionLT` `toSSet`	—	`Set.ext` `mem_degenerate_iff` `SSet.degenerate_eq_top_of_hasDimensionLT`
`le_iff_of_hasDimensionLT` 📖	mathematical	—	`SSet.Subcomplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Set` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Opposite.op` `Set.instHasSubset` `Set.instInter` `CategoryTheory.Subfunctor.obj` `SSet.nonDegenerate`	—	`le_iff_contains_nonDegenerate` `SSet.dim_lt_of_nonDegenerate` `Subtype.prop`

---

← Back to Index