inv — Mathlib

English

If f and g are Θ-equivalent along l, then their pointwise inverses are also Θ-equivalent along l.

Русский

Если f и g эквивалентны по Θ вдоль l, то их обратные по точке функции тоже эквивалентны по Θ вдоль l.

LaTeX

$$$ (f =Θ[l] g) \Rightarrow ((x \mapsto f(x))^{-1} =Θ[l] (x \mapsto g(x))^{-1}). $$$

Lean4

theorem inv {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹ :=
  ⟨h.2.inv_rev h.1.eq_zero_imp, h.1.inv_rev h.2.eq_zero_imp⟩

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