pointwise): Inf and Sup of `a • s` for `s : set ℝ` (#9707)

Commit

4 years ago

feat(data/real/pointwise): Inf and Sup of `a • s` for `s : set ℝ` (#9707) This relates `Inf (a • s)`/`Sup (a • s)` with `a • Inf s`/`a • Sup s` for `s : set ℝ`.

Author

YaelDillies

Parents

e8413250

mathlib 06179ca9 - feat(data/real/pointwise): Inf and Sup of `a • s` for `s : set ℝ` (#9707)

mathlib
06179ca9 - feat(data/real/pointwise): Inf and Sup of `a • s` for `s : set ℝ` (#9707)