div — Mathlib

English

If f =Θ_l g, then for every integer n, f^n =Θ_l g^n.

Русский

Если f =Θ_l g, то для любого целого числа n выполняется f^n =Θ_l g^n.

LaTeX

$$$ (f =Θ[l] g) \Rightarrow (\forall n \in \mathbb{Z}, f^{n} =Θ[l] g^{n}). $$$

Lean4

theorem div {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
    (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x := by simpa only [div_eq_mul_inv] using h₁.mul h₂.inv

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