supConvergenceClass — Mathlib

English

OrderDual of α has SupConvergenceClass if α has it.

Русский

Пусть α имеет SupConvergenceClass; тогда его двойственный порядок имеет SupConvergenceClass.

LaTeX

$$$\\text{SupConvergenceClass}(\\alpha^{\\mathrm{op}}) \\;\\text{given } \\text{InfConvergenceClass}(\\alpha).$$$

Lean4

instance supConvergenceClass [Preorder α] [TopologicalSpace α] [InfConvergenceClass α] : SupConvergenceClass αᵒᵈ :=
  ⟨‹InfConvergenceClass α›.1⟩

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