infConvergenceClass — Mathlib

English

OrderDual of α has InfConvergenceClass if α has SupConvergenceClass.

Русский

Двойственный порядок α имеет InfConvergenceClass, если у α есть SupConvergenceClass.

LaTeX

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

Lean4

instance infConvergenceClass [Preorder α] [TopologicalSpace α] [SupConvergenceClass α] : InfConvergenceClass αᵒᵈ :=
  ⟨‹SupConvergenceClass α›.1⟩
    -- see Note [lower instance priority]

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