isTheta_const_const_iff — Mathlib

English

For any nonzero c in a normed field, (f: α→𝕜) with f =Θ_l g is equivalent to (c·f) =Θ_l g.

Русский

Для любого ненулевого c в нормированном поле, если f =Θ_l g, то (c·f) =Θ_l g эквивалентно f =Θ_l g.

LaTeX

$$$ c \neq 0 \Rightarrow (f =Θ[l] g \Leftrightarrow (c \cdot f) =Θ[l] g). $$$

Lean4

@[simp]
theorem isTheta_const_const_iff [NeBot l] {c₁ : E''} {c₂ : F''} :
    ((fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0) := by
  simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm

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