Commit 2025-04-23 20:10 f685e3a9

View on Github →

feat: under ConditionallyCompleteLinearOrderBot, an order iso preserves suprema unconditionally (#24324) ... thanks to the junk values

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem ciInf_eq_univ_of_not_bddBelow

added theorem ciInf_of_not_bddBelow

added theorem ciSup_eq_univ_of_not_bddAbove

added theorem ciSup_of_not_bddAbove

modified theorem csInf_eq_univ_of_not_bddBelow

modified theorem csInf_of_not_bddBelow

modified theorem csSup_eq_univ_of_not_bddAbove

modified theorem csSup_of_not_bddAbove

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem OrderIso.map_ciSup'