continuousSup — Mathlib

English

If L is a lattice with a topology, and infimum is continuous, then in the dual order Lᵒᵈ the supremum operation is continuous.

Русский

Если у L есть топология и инфимум (наименьшее) непрерывен, то в двойственном порядке Lᵒᵈ операция наибольшего (supremum) непрерывна.

LaTeX

$$$\\text{ContinuousSup}(L^{\\mathrm{op}})$$$

Lean4

instance (priority := 100) continuousSup (L : Type*) [TopologicalSpace L] [Min L] [ContinuousInf L] : ContinuousSup Lᵒᵈ
    where
  continuous_sup :=
    @ContinuousInf.continuous_inf L _ _
      _
        -- see Note [lower instance priority]

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