isBigO_comp_ofReal_nhds_ne — Mathlib

English

If f,g: ℂ → ℂ satisfy f =O_{𝓝[≠](x : ℂ)} g, then (λ 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[𝓝[\\neq] (x : \\mathbb{C})]\\ g \\Rightarrow (\\lambda y: \\mathbb{R}. f\\, y) =O[𝓝[\\neq] x] (\\lambda y: \\mathbb{R}. g\\, y) $$$

Lean4

theorem isBigO_comp_ofReal_nhds_ne {f g : ℂ → ℂ} {x : ℝ} (h : f =O[𝓝[≠] (x : ℂ)] g) :
    (fun y : ℝ ↦ f y) =O[𝓝[≠] x] (fun y : ℝ ↦ g y) :=
  h.comp_tendsto <| continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin fun _ _ ↦ by simp_all

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