English
Let f be a family of functions f_i, then f = o of g in the product sense iff each coordinate f_i = o of g.
Русский
Пусть f — семейство функций f_i; тогда f = o(g) по произведению эквивалентно тому, что каждая координата f_i = o(g).
LaTeX
$$$ f: (i \to E_i) \;\text{and}\; g:\alpha\to F,\; \ f =o_{𝕜;l} g \iff ∀ i, f_i =o_{𝕜;l} g.$$$
Lean4
protected theorem pi {ι : Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
[∀ i, TopologicalSpace (E i)] [∀ i, ContinuousSMul 𝕜 (E i)] {f : ∀ i, α → E i} (h : ∀ i, f i =o[𝕜; l] g) :
(fun x i ↦ f i x) =o[𝕜; l] g :=
by
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
rw [← nhds_pi, ← Pi.zero_def] at this
simp only [this.isLittleOTVS_iff (basis_sets _), forall_and, Prod.forall, id]
rintro I U ⟨hIf, hU, Ub⟩
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩
refine ⟨V, hV₀, fun ε hε ↦ ?_⟩
refine (hIf.eventually_all.mpr (hV · · ε hε)).mono fun x hx ↦ ?_
simpa only [id, egauge_pi hIf Ub, iSup₂_le_iff]
