isTheta_zero_left — Mathlib

English

The constant zero function on the left is Θ-equivalent to a function if and only if that function is eventually zero.

Русский

Левый константный нуль равен Θ-отношению с функцией тогда и только тогда, когда функция стягивается к нулю на языке л.

LaTeX

$$$ (\text{IsTheta l } 0 \ f' ∼) \iff f' \text{ тяготеет к } 0. $$$

Lean4

@[simp]
theorem isTheta_zero_left : (fun _ ↦ (0 : E')) =Θ[l] g'' ↔ g'' =ᶠ[l] 0 := by
  simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and]

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