Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-15 08:37 5c954e12

View on Github →

chore(order/conditionally_complete_lattice): General cleanup (#13319)

Estimated changes

Modified src/order/conditionally_complete_lattice.lean

modified theorem cInf_eq_of_forall_ge_of_forall_gt_exists_lt

modified theorem cInf_le_cInf

modified theorem cInf_le_of_le

modified theorem cInf_lt_of_lt

modified theorem cSup_eq_of_forall_le_of_forall_lt_exists_gt

modified theorem cSup_eq_of_is_forall_le_of_forall_le_imp_ge

modified theorem cSup_inter_le

modified theorem cSup_le

modified theorem cSup_le_cSup

modified theorem cSup_le_iff

modified theorem csupr_const

modified theorem csupr_le

modified theorem exists_lt_of_cInf_lt

modified theorem exists_lt_of_cinfi_lt

modified theorem exists_lt_of_lt_cSup

modified theorem exists_lt_of_lt_csupr

modified theorem le_cInf

modified theorem le_cInf_iff

modified theorem le_cInf_inter

modified theorem le_cSup_of_le

modified theorem le_cinfi

modified theorem lt_cSup_of_lt

modified theorem with_top.coe_Inf

modified theorem with_top.coe_Sup