Commit 2026-08-10 08:17 2b34bbd7

View on Github →

chore(order/ConditionallyCompleteLattice): use to_dual more (#41558) This PR uses to_dual in most remaining places in Mathlib.Order.ConditionallyCompleteLattice.Basic.

Estimated changes

deleted theorem AntitoneOn.sSup_image_Icc
deleted theorem MonotoneOn.sSup_image_Icc
deleted theorem WithBot.sSup_empty
modified theorem WithTop.coe_sSup'
modified theorem WithTop.sInf_empty
modified theorem WithTop.sInf_eq
modified theorem WithTop.sInf_singleton_top
modified theorem WithTop.sSup_empty
modified theorem WithTop.sSup_eq
modified theorem WithTop.sSup_of_top_mem
modified theorem WithTop.sSup_singleton_top
deleted theorem ciInf_of_not_bddBelow
modified theorem ciSup_of_not_bddAbove
deleted theorem csInf_Ioc
deleted theorem csInf_Ioi
deleted theorem csInf_Ioo
deleted theorem csInf_eq_bot_of_bot_mem
deleted theorem csInf_insert
deleted theorem csInf_le_csInf
deleted theorem csInf_le_iff
deleted theorem csInf_lt_iff
deleted theorem csInf_lt_of_lt
deleted theorem csInf_of_not_bddBelow
deleted theorem csInf_pair
deleted theorem csInf_union
deleted theorem csInf_upperBounds_range
modified theorem csSup_of_not_bddAbove
deleted theorem exists_lt_of_csInf_lt
deleted theorem le_csInf_iff
deleted theorem le_csInf_inter
modified theorem le_csSup_iff
deleted theorem notMem_of_csSup_lt
deleted theorem sInf_iUnion_Ici