isTheta_inv — Mathlib

English

If f1 =Θ_l g1 and f2 =Θ_l g2, then the quotient f1/f2 is Θ_l g1/g2.

Русский

Если f1 =Θ_l g1 и f2 =Θ_l g2, тогда частное f1/f2 равно Θ_l g1/g2.

LaTeX

$$$ (f_1 =Θ[l] g_1) \, and \, (f_2 =Θ[l] g_2) \Rightarrow (f_1/f_2) =Θ[l] (g_1/g_2). $$$

Lean4

@[simp]
theorem isTheta_inv {f : α → 𝕜} {g : α → 𝕜'} : ((fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹) ↔ f =Θ[l] g :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, IsTheta.inv⟩

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