Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 10:03 0ee36a39

View on Github →

feat(order/conditionally_complete_lattice): add lemmas (#9237)

  • add lemmas about conditionally_complete_linear_order_bot; in this case we can drop some nonempty assumptions;
  • add lemmas for the case of [is_well_order α (<)]; in this case infimum of a nonempty set is the least element of this set.

Estimated changes

added theorem Inf_eq_argmin_on
added theorem Inf_mem
added theorem cSup_le'
added theorem cSup_le_iff'
added theorem csupr_le'
added theorem csupr_le_iff'
added theorem exists_lt_of_lt_cSup'
added theorem exists_lt_of_lt_csupr'
modified theorem is_glb.cinfi_eq
added theorem is_least_Inf
added theorem is_lub_cSup'
added theorem le_cInf_iff'