Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-26 08:25 71dcb642

View on Github →

feat(order/conditionally_complete_lattice): add lemmas (#7689) These lemmas names match the version that already exist without the c prefix. This also renames finset.sup_eq_Sup to finset.sup_id_eq_Sup, and introduces a new finset.sup_eq_Sup_image.

Estimated changes

deleted theorem finset.inf_eq_Inf
added theorem finset.inf_id_eq_Inf
deleted theorem finset.sup_eq_Sup
added theorem finset.sup_id_eq_Sup
modified theorem infi_true
modified theorem supr_true
modified theorem cSup_empty
added theorem cinfi_le_of_le
added theorem cinfi_pos
added theorem csupr_neg
added theorem csupr_pos
added theorem finset.inf'_id_eq_cInf
added theorem finset.sup'_id_eq_cSup
added theorem le_csupr_of_le
modified theorem with_bot.cSup_empty
added theorem with_top.cInf_empty