lowerSet — Mathlib

English

Let α be a preorder. Define a topology on α whose open sets are exactly the lower sets.

Русский

Пусть α — предорядок. Определим на α топологию, чьими открытыми множествами будут ровно нижние множества.

LaTeX

$$$\mathcal{T} = \{ U \subseteq \alpha \mid U \text{ is a lower set} \}\quad\Rightarrow\quad (\alpha, \mathcal{T}) \text{ is a topological space}$$$

Lean4

/-- Topology whose open sets are lower sets.

Note: In general the lower set topology does not coincide with the lower topology. -/
def lowerSet (α : Type*) [Preorder α] : TopologicalSpace α
    where
  IsOpen := IsLowerSet
  isOpen_univ := isLowerSet_univ
  isOpen_inter _ _ := IsLowerSet.inter
  isOpen_sUnion _ := isLowerSet_sUnion

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