Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-01 00:20 742ec88c

View on Github →

feat(data/set/*): lemmas about monotone/antitone and sets/intervals (#11173)

  • Rename set.monotone_inter and set.monotone_union to monotone.inter and monotone.union.
  • Add antitone versions of some monotone lemmas.
  • Specialize Union_Inter_of_monotone for set.pi.
  • Add lemmas about ⋃ x, Ioi (f x), ⋃ x, Iio (f x), and ⋃ x, Ioo (f x) (g x).
  • Add dot notation lemmas monotone.Ixx and antitone.Ixx.

Estimated changes

added theorem is_glb.Union_Ioi_eq
added theorem is_glb.bUnion_Ioi_eq
added theorem is_lub.Union_Iio_eq
added theorem is_lub.bUnion_Iio_eq
added theorem antitone_Ici
added theorem antitone_Ioi
added theorem monotone_Iic
added theorem monotone_Iio
added theorem antitone.inter
added theorem antitone.union
added theorem monotone.inter
added theorem monotone.union
added theorem set.antitone_set_of
deleted theorem set.monotone_inter
deleted theorem set.monotone_union
added theorem antitone.le_map_inf
added theorem antitone.map_inf
added theorem antitone.map_sup
added theorem antitone.map_sup_le