Commit 2025-01-22 08:02 e0e86050

View on Github →

chore(CategoryTheory): move Functor.IsWellOrderContinuous (#20366) The definition of Functor.IsWellOrderContinuous is moved to a better place Limits.Shapes.Preorder.WellOrderContinuous (see also #20335).

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean

added def CategoryTheory.Functor.coconeLT

added theorem CategoryTheory.Functor.isWellOrderContinuous_of_iso

added def CategoryTheory.Functor.restrictionLT

Modified Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

deleted def CategoryTheory.Functor.coconeLT

deleted theorem CategoryTheory.Functor.isWellOrderContinuous_of_iso

deleted def CategoryTheory.Functor.restrictionLT

Modified Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean