isBoundedUnder_ge — Mathlib

English

If a function u : ι → α tends to a along a filter f, then the image is bounded under the relation ≥ along f.

Русский

Если функция u: ι → α сходится к a вдоль фильтра f, то образ (множество значений u) ограничено снизу по отношению к ≥ вдоль f.

LaTeX

$$$ (h: \mathrm{Tendsto}\, u\, f\, (\mathcal{N}a)) \\Rightarrow \\ f.IsBoundedUnder (\ge) u. $$$

Lean4

theorem isBoundedUnder_ge (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≥ ·) u :=
  (isBounded_ge_nhds a).mono h

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