inv_rev — Mathlib

English

If f = o_l g, then (g)^{-1} = o_l (f)^{-1} under a zero-pairing compatibility condition.

Русский

Если f = o_l g, то 1/g = o_l 1/f при условии совместимости нулевых точек.

LaTeX

$$f =o_l g \\Rightarrow g^{-1} =o_l f^{-1} \\text{ under } (\\forall^\\infty x\\in l,\ f(x)=0 \\Rightarrow g(x)=0).$$

Lean4

theorem inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : f =o[l] g) (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
    (fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹ :=
  IsLittleO.of_isBigOWith fun _c hc => (h.def' hc).inv_rev h₀

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