Theorems · Definition · general topology

Topology.IsUpper.upperBasis

(α : Type u_3) → [Preorder α] → Set (Set α)

The complements of the lower closures of finite sets are a collection of upper sets which form a basis for the upper topology.

Defined in

Mathlib.Topology.Order.LowerUpperTopology

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

Preorder