English
If α and β are preordered topological spaces each with a SupConvergenceClass, then their product α × β also has a SupConvergenceClass.
Русский
Если пространства с упорядочением и топологией имеют свойство SupConvergenceClass, то их произведение α×β тоже имеет это свойство.
LaTeX
$$$ (\text{SupConvergenceClass } \alpha) \wedge (\text{SupConvergenceClass } \beta) \Rightarrow \text{SupConvergenceClass}(\alpha \times \beta) $$$
Lean4
instance supConvergenceClass [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [SupConvergenceClass α]
[SupConvergenceClass β] : SupConvergenceClass (α × β) :=
by
constructor
rintro ⟨a, b⟩ s h
rw [isLUB_prod, ← range_restrict, ← range_restrict] at h
have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) := tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) := tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
exact A.prodMk_nhds B
