Commit 2026-09-01 10:16 2cd8f833

View on Github →

chore(ConditionallyCompleteLattice/Indexed): dualize (#38938)

Estimated changes

deleted theorem GaloisConnection.u_ciInf
deleted theorem GaloisConnection.u_csInf'
deleted theorem GaloisConnection.u_csInf
deleted theorem IsGLB.ciInf_eq
deleted theorem IsGLB.ciInf_set_eq
deleted theorem OrderIso.map_ciInf
deleted theorem OrderIso.map_ciInf_set
deleted theorem OrderIso.map_csInf'
deleted theorem OrderIso.map_csInf
deleted theorem Set.Ici_ciSup
deleted theorem WithBot.ciSup_empty
deleted theorem WithBot.coe_iInf
deleted theorem WithBot.coe_iSup
modified theorem WithTop.iInf_empty
deleted theorem cbiInf_eq_ciInf_subtype
deleted theorem cbiInf_eq_of_not_forall
deleted theorem cbiInf_id
deleted theorem cbiInf_of_not_bddBelow
deleted theorem ciInf_and
deleted theorem ciInf_ciInf_eq_left_le
deleted theorem ciInf_ciInf_eq_right_le
deleted theorem ciInf_eq_bot_of_bot_mem
deleted theorem ciInf_image
deleted theorem ciInf_inf_eq
deleted theorem ciInf_inf_le
deleted theorem ciInf_le
deleted theorem ciInf_le_of_le
deleted theorem ciInf_lt_iff
deleted theorem ciInf_mono
deleted theorem ciInf_prod
deleted theorem ciInf_set_le
deleted theorem ciInf_subtype
deleted theorem ciInf_subtype_fun
deleted theorem ciInf₂_le
deleted theorem csInf_image
deleted theorem exists_lt_of_ciInf_lt
deleted theorem le_ciInf_exists
deleted theorem le_ciInf_iff
deleted theorem le_ciInf_set_iff