English
If each α(i) is a Preorder, TopologicalSpace, and SupConvergenceClass, then the function space ∀ i, α(i) has SupConvergenceClass.
Русский
Если для каждого i пространства α(i) обладает свойством SupConvergenceClass, то пространство функций ∀ i α(i) тоже обладает SupConvergenceClass.
LaTeX
$$$ (\forall i, \text{Preorder}(\alpha(i))) \wedge (\forall i, \text{TopologicalSpace}(\alpha(i))) \wedge (\forall i, \text{SupConvergenceClass}(\alpha(i))) \Rightarrow \SupConvergenceClass(\forall i, \alpha(i)) $$$
Lean4
instance supConvergenceClass {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
[∀ i, SupConvergenceClass (α i)] : SupConvergenceClass (∀ i, α i) :=
by
refine ⟨fun f s h => ?_⟩
simp only [isLUB_pi, ← range_restrict] at h
exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)
