Commit 2025-04-26 09:48 a0dbca20

View on Github →

chore(Order): process some porting notes (#24362)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

Modified Mathlib/Order/Filter/Tendsto.lean

Modified Mathlib/Order/Fin/Basic.lean

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderIso.lt_symm_apply

added theorem OrderIso.symm_apply_lt