Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 13:47 9ce6b9a6

View on Github →

feat(order/complete_lattice): add sup_eq_supr and inf_eq_infi (#8573)

  • add bool.injective_iff, bool.univ_eq, and bool.range_eq;
  • add sup_eq_supr and inf_eq_infi;
  • golf filter.comap_sup.

Estimated changes

added theorem bool.injective_iff
added theorem bool.range_eq
added theorem bool.univ_eq
added theorem inf_eq_infi
added theorem sup_eq_supr