continuousInf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) continuousInf (L : Type*) [TopologicalSpace L] [Max L] [ContinuousSup L] : ContinuousInf Lᵒᵈ
    where continuous_inf := @ContinuousSup.continuous_sup L _ _ _

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