isBigO_comp_ofReal_nhds — Mathlib

English

If f,g: ℂ → ℂ satisfy f =O_{𝓝( x : ℂ)} g, then the real-variable realizations satisfy (y ↦ f(y)) =O_{𝓝 x} (y ↦ g(y)).

Русский

Если f,g: ℂ → ℂ удовлетворяют f =O_{𝓝( x : ℂ)} g, то при рассмотрении в виде функций ℝ → ℂ выполняется (y ↦ f(y)) =O_{𝓝 x} (y ↦ g(y)).

LaTeX

$$$ f =O[𝓝 (x : \\mathbb{C})]\\ g \\Rightarrow (\\lambda y: \\mathbb{R}. f\\, y) =O[𝓝 x] (\\lambda y: \\mathbb{R}. g\\, y) $$$

Lean4

theorem isBigO_comp_ofReal_nhds {f g : ℂ → ℂ} {x : ℝ} (h : f =O[𝓝 (x : ℂ)] g) :
    (fun y : ℝ ↦ f y) =O[𝓝 x] (fun y : ℝ ↦ g y) :=
  h.comp_tendsto <| continuous_ofReal.tendsto x

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