English
Relating IsLittleOTVS on nhdsWithin with an inserted point: if f is little-OTVS near x with respect to a neighborhood and f(x)=0, then IsLittleOTVS remains after inserting x into the neighborhood basis.
Русский
Связь IsLittleOTVS на nhdsWithin после добавления точки: если f мало-относится к x при окрестности и f(x)=0, то IsLittleOTVS сохраняется.
LaTeX
$$$\\text{IsLittleOTVS}(\\text{nhdsWithin } x (\\text{insert } x s)) f g \\iff \\text{IsLittleOTVS}(\\text{nhdsWithin } x s) f g.$$$
Lean4
theorem prodMk [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) :
(fun x ↦ (f x, g x)) =o[𝕜; l] k :=
by
rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isLittleOTVS_iff (basis_sets _)]
rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩
rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets with
⟨W, hW, hWf, hWg⟩
refine ⟨W, hW, fun ε hε ↦ ?_⟩
filter_upwards [hWf ε hε, hWg ε hε] with x hfx hgx
simp [egauge_prod_mk, *]
