Commit 2024-12-20 13:13 949bc42a

View on Github →

feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions (#19306)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.of_eq

Created Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

added def CategoryTheory.Functor.coconeLT

added theorem CategoryTheory.Functor.isWellOrderContinuous_of_iso

added def CategoryTheory.Functor.restrictionLT

added theorem CategoryTheory.MorphismProperty.mem_of_transfinite_composition

added inductive CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le