Commit 2026-04-18 08:20 9eb6feb6

View on Github →

feat(AlgebraicTopology/SimplicialSet): anodyne extensions (#37321)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Basic.lean

added theorem SSet.Subcomplex.Pairing.anodyneExtensions

added theorem SSet.Subcomplex.Pairing.strongAnodyneExtensions

added theorem SSet.anodyneExtensions.horn_ι

added theorem SSet.anodyneExtensions.of_isIso

added def SSet.anodyneExtensions

added theorem SSet.anodyneExtensions_eq_llp_rlp

added theorem SSet.anodyneExtensions_eq_retracts_transfiniteCompositions

added theorem SSet.anodyneExtensions_eq_retracts_transfiniteCompositionsOfShape

added def SSet.strongAnodyneExtensions

added theorem SSet.strongAnodyneExtensions_le_anodyneExtensions

added theorem SSet.strongAnodyneExtensions_ι_iff

Modified Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean

modified theorem SSet.modelCategoryQuillen.horn_ι_mem_J

Modified Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean

Modified Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

Modified Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

added theorem CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0

Modified Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean