upperSet — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Topology whose open sets are upper sets.

Note: In general the upper set topology does not coincide with the upper topology. -/
def upperSet (α : Type*) [Preorder α] : TopologicalSpace α
    where
  IsOpen := IsUpperSet
  isOpen_univ := isUpperSet_univ
  isOpen_inter _ _ := IsUpperSet.inter
  isOpen_sUnion _ := isUpperSet_sUnion

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