Commit 2026-06-02 12:39 25640221

View on Github →

chore(Order/CompleteLattice/Lemmas): use to_dual (#37752) Use to_dual for lemmas about CompleteLattice.

Estimated changes

deleted theorem ULift.down_iInf
deleted theorem ULift.down_sInf
deleted theorem ULift.up_iInf
deleted theorem ULift.up_sInf
deleted theorem biSup_inf_le_biSup_inf
deleted theorem biSup_inf_le_inf_biSup
deleted theorem iInf_bool_eq
deleted theorem iInf_ge_eq_iInf_nat_add
deleted theorem iSup_inf_le_iSup_inf
deleted theorem iSup_inf_le_inf_iSup
deleted theorem iSup_inf_le_inf_sSup
deleted theorem iSup_inf_le_sSup_inf
deleted theorem iSup_nat_gt_zero_eq
deleted theorem inf_eq_iInf
deleted theorem inf_iInf_nat_succ
deleted theorem le_iSup_inf_iSup