isBoundedUnder_of_range — Mathlib

English

If the range of u is bounded below, then f is bounded under ≥ by u for any filter f.

Русский

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

LaTeX

$$$ BddBelow (Set.range u) \Rightarrow \forall f, f.IsBoundedUnder (\ge) u $$$

Lean4

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

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