mathlib

35b67fd9 - feat(algebra/order/field, data/real/basic): lemmas about `Sup` and `is_lub` (#11013)

feat(algebra/order/field, data/real/basic): lemmas about `Sup` and `is_lub` (#11013) Add a lemma stating that for `f : α → ℝ` with `α` empty, `(⨆ i, f i) = 0`; a lemma stating that in an ordered field `is_lub` scales under multiplication by a nonnegative constant, and some variants.