isBigO_const_of_tendsto — Mathlib

English

Let y be a point of E'' and suppose f'' converges to y along l. If c ≠ 0, then f'' = O_l (λ x, c).

Русский

Пусть y ∈ E'' и f'' сходится к y вдоль l. Пусть c ≠ 0. Тогда f'' = O_l (λ x, c).

LaTeX

$$$ \text{Tendsto } f''\ l\ (\mathcal{N}y) \quad \land \ c \neq 0 \Longrightarrow f'' =O[l](\lambda _.\, c). $$$

Lean4

theorem isBigO_const_of_tendsto {y : E''} (h : Tendsto f'' l (𝓝 y)) {c : F''} (hc : c ≠ 0) : f'' =O[l] fun _x => c :=
  h.norm.isBoundedUnder_le.isBigO_const hc

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