topologicalLattice — Mathlib

English

In a linear order with OrderClosedTopology, both min and max are continuous; hence the structure is a topological lattice.

Русский

Для линейного порядка с OrderClosedTopology операции min и max непрерывны; следовательно, образуется топологическая решетка.

LaTeX

$$$\\text{continuous\_inf} = \\text{continuous\_min}$ и $\\text{continuous\_sup} = \\text{continuous\_max}$, т.е. обе операции непрерывны.$$

Lean4

instance (priority := 100) topologicalLattice {L : Type*} [TopologicalSpace L] [LinearOrder L] [OrderClosedTopology L] :
    TopologicalLattice L where
  continuous_inf := continuous_min
  continuous_sup := continuous_max

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