IsOpen — Mathlib

English

An open set in the Scott topology is exactly one whose membership predicate is ωScottContinuous.

Русский

Открытое множество в Scott-топологии есть ровно то множество, чья характеристическая функция является ωScott-непрерывной.

LaTeX

$$$IsOpen(s) \;\text{ is defined by } \; IsOpen(s) \equiv \omegaScottContinuous(\lambda x. x \in s).$$$

Lean4

/-- The characteristic function of open sets is monotone and preserves
the limits of chains. -/
def IsOpen (s : Set α) : Prop :=
  ωScottContinuous fun x ↦ x ∈ s

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