insert — Mathlib

English

If g(x) = 0, then restricting to a neighborhood with an insertion preserves the Little-O relation: g = o in nhdsWithin x s implies g = o in nhdsWithin x with x inserted.

Русский

Если g(x) = 0, то переход к окрестности с вставкой сохраняет отношение Little-O: g = o в nhdsWithin x s следует g = o в nhdsWithin x с вставкой x.

LaTeX

$$$\text{If } g(x)=0,\; g = o_{nhdsWithin(x, s)}\; f \iff g = o_{nhdsWithin(x, insert~x~s)}\; f$$$

Lean4

protected theorem insert [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h1 : g =o[𝓝[s] x] g')
    (h2 : g x = 0) : g =o[𝓝[insert x s] x] g' :=
  (isLittleO_insert h2).mpr h1

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