Commit 2025-12-08 13:24 716ac686

View on Github →

feat(AlgebraicTopology): dimension of simplicial sets (#32201) For a simplicial set X and d : ℕ, we introduce a typeclass X.HasDimensionLT d saying that the dimension of X is < d, i.e. all nondegenerate simplices of X are of dimension < d.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/Dimension.lean

added theorem SSet.Subcomplex.eq_top_iff_of_hasDimensionLT

added theorem SSet.Subcomplex.hasDimensionLT_of_le

added theorem SSet.Subcomplex.le_iff_of_hasDimensionLT

added theorem SSet.degenerate_eq_top_of_hasDimensionLT

added theorem SSet.dim_le_of_nonDegenerate

added theorem SSet.dim_lt_of_nonDegenerate

added theorem SSet.hasDimensionLT_iSup_iff

added theorem SSet.hasDimensionLT_iff_of_iso

added theorem SSet.hasDimensionLT_of_epi

added theorem SSet.hasDimensionLT_of_le

added theorem SSet.hasDimensionLT_of_mono

added theorem SSet.hasDimensionLT_subcomplex_top_iff

added theorem SSet.nonDegenerate_eq_bot_of_hasDimensionLT

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean