Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-02 04:57 4884ea53

View on Github →

feat(order/[conditionally_]complete_lattice): add more intro lemmas for [c][Sup, Inf] and [c][supr, infi] (#7730)

Estimated changes

Modified src/order/complete_lattice.lean

added theorem Inf_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem Sup_eq_of_forall_le_of_forall_lt_exists_gt

added theorem infi_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem supr_eq_of_forall_le_of_forall_lt_exists_gt

Modified src/order/conditionally_complete_lattice.lean

added theorem cInf_eq_of_forall_ge_of_forall_gt_exists_lt

deleted theorem cInf_intro

added theorem cSup_eq_of_forall_le_of_forall_lt_exists_gt

added theorem cSup_eq_of_is_forall_le_of_forall_le_imp_ge

deleted theorem cSup_intro'

deleted theorem cSup_intro

added theorem cinfi_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem csupr_eq_of_forall_le_of_forall_lt_exists_gt

Modified src/topology/algebra/ordered/liminf_limsup.lean