Commit 2026-06-02 12:39 e6346c5c

feat(Order/ConditionallyCompleteLattice/Basic): more WithTop instances (#38890) Adds the following instances:

CompleteLattice α → CompleteLattice (WithTop α)
CompleteLinearOrder α → CompleteLinearOrder (WithBot α)
ConditionallyCompleteLinearOrder α → ConditionallyCompleteLinearOrder (WithTop α)
ConditionallyCompleteLinearOrder α → ConditionallyCompleteLinearOrderBot (WithBot α)

and some simp lemmas to help.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted theorem Monotone.csInf_image_le

deleted theorem Monotone.le_csInf_image

deleted theorem WithBot.coe_sInf'

deleted theorem WithBot.coe_sSup'

deleted theorem WithBot.sInf_empty

deleted theorem WithBot.sInf_eq

deleted theorem WithBot.sSup_eq

modified theorem WithTop.coe_sInf'

added theorem WithTop.sInf_of_not_bddBelow

added theorem WithTop.sInf_singleton_top

added theorem WithTop.sSup_empty

added theorem WithTop.sSup_of_not_bddAbove

added theorem WithTop.sSup_of_top_mem

added theorem WithTop.sSup_singleton_top