mathlib3
742ec88c - feat(data/set/*): lemmas about `monotone`/`antitone` and sets/intervals (#11173)

Commit
4 years ago
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`.
Author
Parents
Loading