lawson — Mathlib

English

The Lawson topology on a preordered set α is defined as the infimum of the lower topology and the Scott topology (on univ).

Русский

Лоусоновская топология на предордере α определяется как исчерпаемость нижней топологии и топологии Скотта (на множестве all).

LaTeX

$$$\operatorname{lawson}(\alpha) = \operatorname{lower}(\alpha) \;\inf\; \operatorname{scott}(\alpha, \mathrm{univ}).$$$

Lean4

/-- The Lawson topology is defined as the meet of `Topology.lower` and the `Topology.scott`.
-/
def lawson (α : Type*) [Preorder α] : TopologicalSpace α :=
  lower α ⊓ scott α univ

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