topology — Mathlib

English

If α is a preorder, define a topology on α generated by the subbase consisting of all sets {x ∈ α | a < x} and {x ∈ α | x < b} for all a,b ∈ α.

Русский

Если α задано как частичный порядок, задаём топологию на α, порождающуюся подоснобом, состоящим из всех множеств {x ∈ α | a < x} и {x ∈ α | x < b} для всех a,b ∈ α.

LaTeX

$$$\\tau(\\alpha) = \\mathrm{generateFrom}\\{ S \\subseteq \\alpha \\mid \\exists a\\, (S = \\{b\\in\\alpha \\mid a

Lean4

/-- (Order) topology on a partial order `α` generated by the subbase of open intervals
`(a, ∞) = { x ∣ a < x }, (-∞, b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary. -/
def topology (α : Type*) [Preorder α] : TopologicalSpace α :=
  generateFrom {s : Set α | ∃ a : α, s = {b : α | a < b} ∨ s = {b : α | b < a}}

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