isLittleOTVS_insert — Mathlib

English

The zero function is little-OTVS relative to any target function: the ratio tends to zero in the IsLittleOTVS sense.

Русский

Нулевая функция является little-OTVS по отношению к любой функции-цели: отношение стремится к нулю.

LaTeX

$$$(0 : \\alpha \\to E) =o[𝕜; l] g.$$$

Lean4

theorem isLittleOTVS_insert [TopologicalSpace α] {x : α} {s : Set α} (h : f x = 0) :
    f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; (𝓝[s] x)] g :=
  by
  rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]
  exact .congr' (.zero g _) h.symm .rfl

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