isTheta_const_const — Mathlib

English

If c ≠ 0 in a normed field and f and g’ satisfy f =Θ_l (c · g'), then f =Θ_l g'.

Русский

Если c ≠ 0 в нормированном поле и f =Θ_l (c · g'), то f =Θ_l g'.

LaTeX

$$$ (f =Θ[l] (c·g')) \Rightarrow (f =Θ[l] g'). $$$

Lean4

theorem isTheta_const_const {c₁ : E''} {c₂ : F''} (h₁ : c₁ ≠ 0) (h₂ : c₂ ≠ 0) : (fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂ :=
  ⟨isBigO_const_const _ h₂ _, isBigO_const_const _ h₁ _⟩

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