isBoundedUnder_of_range — Mathlib

English

If the range of u is bounded above, then u is f-bounded above for any filter f.

Русский

Если множество значений u ограничено сверху, то u ограничено сверху по любому фильтру f.

LaTeX

$$$ BddAbove (Set.range u) \Rightarrow \forall f, f.IsBoundedUnder (\le) u $$$

Lean4

/-- A bounded above function `u` is in particular eventually bounded above. -/
theorem _root_.BddAbove.isBoundedUnder_of_range (hu : BddAbove (Set.range u)) : f.IsBoundedUnder (· ≤ ·) u :=
  BddAbove.isBoundedUnder (s := univ) f.univ_mem (by simpa)

Похожие утверждения