toTopologicalLattice — Mathlib

English

A normed lattice-ordered group is a topological lattice with respect to the norm topology.

Русский

Нормированная решётка-группа образует топологическую решётку в нормовой топологии.

LaTeX

$$$\text{TopologicalLattice } \alpha$$$

Lean4

/-- Let `α` be a normed lattice ordered group. Then `α` is a topological lattice in the norm topology.
-/
instance (priority := 100) toTopologicalLattice : TopologicalLattice α :=
  TopologicalLattice.mk

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