Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-01 09:36 5b9b4557

View on Github →

chore(order/complete_lattice): generalize Sup_eq_supr', add lemmas (#8484)

  • Sup_eq_supr' only needs [has_Sup α], add Inf_eq_infi';
  • add supr_range', infi_range', Sup_image', Inf_image' lemmas that use supremum/infimum over subtypes and only require [has_Sup]/[has_Inf].

Estimated changes

added theorem Inf_eq_infi'
added theorem Inf_image'
modified theorem Sup_eq_supr'
added theorem Sup_image'
added theorem infi_range'
added theorem supr_range'