insert — Mathlib

English

If a pair of functions (f, g) is little-OTVS relative to k, then each projection to f or to g retains the little-OTVS relation with k separately.

Русский

Если пара функций (f, g) является little-OTVS по отношению к k, то каждая проекция сохраняет отношение little-OTVS относительно k по-отдельности.

LaTeX

$$$f =o[𝕜; l] k \\Rightarrow (f \\text{ fst}) =o[𝕜; l] k$ and similarly for snd.$$

Lean4

theorem insert [TopologicalSpace α] {x : α} {s : Set α} (h : f =o[𝕜; 𝓝[s] x] g) (hf : f x = 0) :
    f =o[𝕜; 𝓝[insert x s] x] g :=
  (isLittleOTVS_insert hf).2 h

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