English
If α and β are indexed families with Preorder, TopologicalSpace, and InfConvergenceClass, then their product has InfConvergenceClass.
Русский
Если две семействования с упорядочиванием, топологией и InfConvergenceClass, то их произведение обладает InfConvergenceClass.
LaTeX
$$$ (\text{Preorder } \alpha) \wedge (\text{TopologicalSpace } \alpha) \wedge (\text{InfConvergenceClass } \alpha) \wedge (\text{Preorder } \beta) \wedge (\text{TopologicalSpace } \beta) \wedge (\text{InfConvergenceClass } \beta) \Rightarrow \InfConvergenceClass(\alpha \times \beta) $$$
Lean4
instance [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [InfConvergenceClass α]
[InfConvergenceClass β] : InfConvergenceClass (α × β) :=
show InfConvergenceClass (αᵒᵈ × βᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass
