orderClosedTopology — Mathlib

English

In any HasSolidNorm structure on a lattice-ordered normed group, the underlying topology is order-closed.

Русский

В структуре HasSolidNorm на решётчатой нормированной группе топология совместима с порядком и является порядкоположной.

LaTeX

$$$\text{OrderClosedTopology } E$$$

Lean4

instance (priority := 100) orderClosedTopology {E} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E]
    [IsOrderedAddMonoid E] : OrderClosedTopology E :=
  ⟨isClosed_le_of_isClosed_nonneg isClosed_nonneg⟩

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