isLittleO_const_left — Mathlib

English

For u and v, u = o[l] v iff there exists φ with Tendsto φ to 0 and u = φ·v eventually.

Русский

Для функций u и v верно: u = o[l] v тогда и только тогда, когда существует φ с пределом 0 и u = φ·v почти всюду.

LaTeX

$$$ u =o[l] v \\iff \\exists \\phi : α \\to 𝕜, Tendsto \\phi l (\\mathcal{N} 0) ∧ u =ᶠ[l] \\phi \\cdot v $$$

Lean4

@[simp]
theorem isLittleO_const_left {c : E''} : (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop :=
  by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp only [isLittleO_zero, true_or]
  · simp only [hc, false_or, isLittleO_const_left_of_ne hc]; rfl

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