English
If two coordinate functions are individually Big-OTVS with respect to k, then their product is Big-OTVS with respect to k.
Русский
Если две функции по координатам являются Big-OTVS относительно k, то их произведение — тоже Big-OTVS относительно k.
LaTeX
$$$\\text{IsBigOTVS}(l, f, k) \\land \\text{IsBigOTVS}(l, g, k) \\Rightarrow \\text{IsBigOTVS}(l, (f,g), k).$$$
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)).isBigOTVS_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, ?_⟩
filter_upwards [hWf, hWg] with x hfx hgx
simp [egauge_prod_mk, *]
