lawsonBasis — Mathlib

English

The complements of the upper closures of finite sets intersected with Scott-open sets form a basis for the Lawson topology.

Русский

Комплементы верхних замыканий конечных множеств, пересеченные с открытыми множества́ми Скотта, образуют базис Лоусоновой топологии.

LaTeX

$$$\text{lawsonBasis}(\alpha) = \{ s \subseteq \alpha \mid \exists t,\ t\text{Finite } \land \exists u,\ IsOpen[scott(\alpha, univ)](u) \land u \setminus \overline{t} = s\}.$$$

Lean4

/-- The complements of the upper closures of finite sets intersected with Scott open sets form
a basis for the lawson topology. -/
def lawsonBasis :=
  {s : Set α | ∃ t : Set α, t.Finite ∧ ∃ u : Set α, IsOpen[scott α univ] u ∧ u \ upperClosure t = s}

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