isCoboundedUnder_le — Mathlib

English

If u f (nhds a), then f is cobounded under ≤ with respect to u.

Русский

Если Tendsto u f (nhds a), то f является ограниченно-верхним относительно ≤ по отношению к u.

LaTeX

$$$ (h: Tendsto\, u\, f\, (\mathcal{N}a)) \Rightarrow f.IsCoboundedUnder (\le) u. $$$

Lean4

theorem isCoboundedUnder_le [NeBot f] (h : Tendsto u f (𝓝 a)) : f.IsCoboundedUnder (· ≤ ·) u :=
  h.isBoundedUnder_ge.isCobounded_flip

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