topologicalLattice — Mathlib

English

The dual of a topological lattice is itself a topological lattice.

Русский

Дуальная упорядоченная топологическая решетка самa по себе является топологической решеткой.

LaTeX

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

Lean4

instance (priority := 100) topologicalLattice (L : Type*) [TopologicalSpace L] [Lattice L] [TopologicalLattice L] :
    TopologicalLattice Lᵒᵈ where
  -- see Note [lower instance priority]

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