infConvergenceClass — Mathlib

English

If every α(i) has InfConvergenceClass, then ∀ i α(i) has InfConvergenceClass.

Русский

Если у каждого i пространство α(i) обладает InfConvergenceClass, то пространство функций ∀ i α(i) обладает InfConvergenceClass.

LaTeX

$$$ (\forall i, \text{Preorder}(\alpha(i))) \wedge (\forall i, \text{TopologicalSpace}(\alpha(i))) \wedge (\forall i, \InfConvergenceClass(\alpha(i))) \Rightarrow \InfConvergenceClass(\forall i, \alpha(i)) $$$

Lean4

instance infConvergenceClass {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, InfConvergenceClass (α i)] : InfConvergenceClass (∀ i, α i) :=
  show InfConvergenceClass (∀ i, (α i)ᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass

Похожие утверждения