Vietoris topology

This file defines the Vietoris topology on the types of compact subsets and nonempty compact subsets of a topological space. The Vietoris topology is generated by sets of the form $\{K \mid K \subseteq U\}$ and $\{K \mid K \cap U \ne \emptyset\}$, where $U$ is an open subset of the underlying space.

Implementation notes

Rather than defining the topology directly on TopologicalSpace.Compacts α, we first define TopologicalSpace.vietoris α on Set α, then we take the subspace topology on TopologicalSpace.Compacts α and TopologicalSpace.NonemptyCompacts α. This approach will let us reuse several results if a type of closed sets equipped with the Vietoris topology is defined in the future.

Note that we do not equip TopologicalSpace.Closeds α with the Vietoris topology. When α is a metric space, TopologicalSpace.Closeds α is equipped with the Hausdorff metric, which is generally incompatible with the Vietoris topology.

References

• Ernest Michael, Topologies on spaces of subsets

def 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.

Equations

• TopologicalSpace.vietoris α = TopologicalSpace.generateFrom (Set.powerset '' {U : Set α | IsOpen U} ∪ (fun (V : Set α) => {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen V})

theorem IsOpen.powerset_vietoris {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen (𝒫 U)

When Set is equipped with the Vietoris topology, the powerset of an open set is open.

theorem TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen {s : Set α | (s ∩ U).Nonempty}

theorem IsClosed.powerset_vietoris {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed (𝒫 F)

When Set is equipped with the Vietoris topology, the powerset of a closed set is closed.

theorem TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {s : Set α | (s ∩ F).Nonempty}

theorem TopologicalSpace.vietoris.isClopen_singleton_empty {α : Type u_1} [TopologicalSpace α] : IsClopen {∅}

instance TopologicalSpace.Compacts.topology {α : Type u_1} [TopologicalSpace α] : TopologicalSpace (Compacts α)

The Vietoris topology on the compact subsets of a topological space.

Equations

• TopologicalSpace.Compacts.topology = TopologicalSpace.induced SetLike.coe (TopologicalSpace.vietoris α)

theorem TopologicalSpace.Compacts.isEmbedding_coe {α : Type u_1} [TopologicalSpace α] : Topology.IsEmbedding SetLike.coe

theorem TopologicalSpace.Compacts.continuous_coe {α : Type u_1} [TopologicalSpace α] : Continuous SetLike.coe

theorem TopologicalSpace.Compacts.isOpen_subsets_of_isOpen {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen {K : Compacts α | ↑K ⊆ U}

theorem TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen {K : Compacts α | (↑K ∩ U).Nonempty}

theorem TopologicalSpace.Compacts.isClosed_subsets_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {K : Compacts α | ↑K ⊆ F}

theorem TopologicalSpace.Compacts.isClosed_inter_nonempty_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {K : Compacts α | (↑K ∩ F).Nonempty}

theorem TopologicalSpace.Compacts.isClopen_singleton_bot {α : Type u_1} [TopologicalSpace α] : IsClopen {⊥}

instance TopologicalSpace.NonemptyCompacts.topology {α : Type u_1} [TopologicalSpace α] : TopologicalSpace (NonemptyCompacts α)

The Vietoris topology on the nonempty compact subsets of a topological space.

Equations

• TopologicalSpace.NonemptyCompacts.topology = TopologicalSpace.induced SetLike.coe (TopologicalSpace.vietoris α)

theorem TopologicalSpace.NonemptyCompacts.isEmbedding_coe {α : Type u_1} [TopologicalSpace α] : Topology.IsEmbedding SetLike.coe

theorem TopologicalSpace.NonemptyCompacts.continuous_coe {α : Type u_1} [TopologicalSpace α] : Continuous SetLike.coe

theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts {α : Type u_1} [TopologicalSpace α] : Topology.IsEmbedding toCompacts

theorem TopologicalSpace.NonemptyCompacts.continuous_toCompacts {α : Type u_1} [TopologicalSpace α] : Continuous toCompacts

theorem TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts {α : Type u_1} [TopologicalSpace α] : Topology.IsClosedEmbedding toCompacts

theorem TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts {α : Type u_1} [TopologicalSpace α] : Topology.IsOpenEmbedding toCompacts

theorem TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen {K : NonemptyCompacts α | ↑K ⊆ U}

theorem TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [TopologicalSpace α] {U : Set α} (h : IsOpen U) : IsOpen {K : NonemptyCompacts α | (↑K ∩ U).Nonempty}

theorem TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {K : NonemptyCompacts α | ↑K ⊆ F}

theorem TopologicalSpace.NonemptyCompacts.isClosed_inter_nonempty_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {K : NonemptyCompacts α | (↑K ∩ F).Nonempty}