upperBasis — Mathlib

English

The complement of the lower closures of finite sets forms a basis for the upper topology.

Русский

Дополнение к нижнему замыканию конечного множества образует базис для верхней топологии.

LaTeX

$$$\\text{upperBasis}(\\alpha) = \\{ s \\subseteq \\alpha \mid \\exists t, t.Finite \\land (\\operatorname{lowerClosure}(t))^{c} = s \\}$$$

Lean4

/-- The complements of the lower closures of finite sets are a collection of upper sets
which form a basis for the upper topology. -/
def upperBasis (α : Type*) [Preorder α] :=
  {s : Set α | ∃ t : Set α, t.Finite ∧ (lowerClosure t : Set α)ᶜ = s}

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