Theorem monotone_inclusion_lt_lt_of_le

Modification history

2025-02-03 20:04
Mathlib/Order/Monotone/Basic.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Deleted monotone_inclusion_lt_lt_of_leView on Github →
2024-07-01 08:42
Mathlib/Order/Monotone/Basic.lean
feat(CategoryTheory/SmallObject): the category of transfinite iterations of a functor (#12211) …
Added monotone_inclusion_lt_lt_of_leView on Github →