Theorems · Definition · general topology

TopologicalSpace.vietoris

(α : Type u_1) → [TopologicalSpace α] → TopologicalSpace (Set α)

The Vietoris topology on the powerset of a topological space, generated by sets of the form {A | A ⊆ U} and {A | A ∩ U ≠ ∅}, where U is an open subset of the underlying space. Used for defining the topologies on Compacts and NonemptyCompacts.

Defined in

Mathlib.Topology.Sets.VietorisTopology

Cited by

34 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

TopologicalSpace