Commit 2025-11-29 05:38 f741387c

View on Github →

feat(Order): coercion to WithBot α commutes with biSup (#26287) The coercion from α to WithBot α commutes with biSup and biInf.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem WithBot.sInf_empty

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem WithBot.coe_biInf

added theorem WithBot.coe_biSup