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][michael1951]

@[implicit_reducible]

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 {∅}

theorem TopologicalSpace.vietoris.isTopologicalBasis {α : Type u_1} [TopologicalSpace α] : IsTopologicalBasis ((fun (u : Set (Set α)) => {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen U})

The Vietoris topology has a basis consisting of sets of the form {s | s ⊆ U₁ ∪ … ∪ Uₙ, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ are open sets.

theorem TopologicalSpace.IsTopologicalBasis.vietoris {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) : IsTopologicalBasis ((fun (p : Set α × Set (Set α)) => {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) '' {p : Set α × Set (Set α) | IsOpen p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})

Given a basis B on the underlying topological space, the Vietoris topology has a basis consisting of sets of the form {s | s ⊆ V, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ ∈ B are subsets of some open set V.

theorem IsCompact.powerset_vietoris {α : Type u_1} [TopologicalSpace α] {K : Set α} (hK : IsCompact K) : IsCompact (𝒫 K)

instance TopologicalSpace.vietoris.instCompactSpaceSet {α : Type u_1} [TopologicalSpace α] [CompactSpace α] : CompactSpace (Set α)

theorem TopologicalSpace.vietoris.specializes_of_subset_closure {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) : s ⤳ t

theorem TopologicalSpace.vietoris.specializes_closure {α : Type u_1} [TopologicalSpace α] {s : Set α} : s ⤳ closure s

@[implicit_reducible]

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 {⊥}

theorem TopologicalSpace.IsTopologicalBasis.compacts {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) : IsTopologicalBasis ((fun (u : Set (Set α)) => {K : Compacts α | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u : Set (Set α) | u.Finite ∧ u ⊆ B})

Given a basis B on a topological space α, the topology of Compacts α has a basis consisting of sets of the form {K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ ∈ B.

theorem TopologicalSpace.Compacts.isTopologicalBasis {α : Type u_1} [TopologicalSpace α] : IsTopologicalBasis ((fun (u : Set (Set α)) => {K : Compacts α | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen U})

The topology of Compacts α has a basis consisting of sets of the form {K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ are open sets.

See also TopologicalSpace.IsTopologicalBasis.compacts for a variant where the sets Uᵢ are chosen from some basis.

theorem TopologicalSpace.Compacts.isCompact_subsets_of_isCompact {α : Type u_1} [TopologicalSpace α] {K : Set α} (hK : IsCompact K) : IsCompact {L : Compacts α | ↑L ⊆ K}

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

theorem TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact {α : Type u_1} [TopologicalSpace α] {S : Set (Compacts α)} (hS : IsCompact S) : IsCompact (⋃ K ∈ S, ↑K)

@[simp]

theorem TopologicalSpace.Compacts.compactSpace_iff {α : Type u_1} [TopologicalSpace α] : CompactSpace (Compacts α) ↔ CompactSpace α

@[simp]

theorem TopologicalSpace.Compacts.noncompactSpace_iff {α : Type u_1} [TopologicalSpace α] : NoncompactSpace (Compacts α) ↔ NoncompactSpace α

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

@[implicit_reducible]

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}

theorem TopologicalSpace.IsTopologicalBasis.nonemptyCompacts {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) : IsTopologicalBasis ((fun (u : Set (Set α)) => {K : NonemptyCompacts α | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})

Given a basis B on a topological space α, the topology of NonemptyCompacts α has a basis consisting of sets of the form {K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ ∈ B and n > 0.

theorem TopologicalSpace.NonemptyCompacts.isTopologicalBasis {α : Type u_1} [TopologicalSpace α] : IsTopologicalBasis ((fun (u : Set (Set α)) => {K : NonemptyCompacts α | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ ∀ U ∈ u, IsOpen U})

The topology of NonemptyCompacts α has a basis consisting of sets of the form {s | s ⊆ U₁ ∪ … ∪ Uₙ, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}, where U₁, …, Uₙ are open sets and n > 0.

See also TopologicalSpace.IsTopologicalBasis.nonemptyCompacts for a variant where the sets Uᵢ are chosen from some basis.

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

theorem TopologicalSpace.NonemptyCompacts.isCompact_subsets_of_isCompact {α : Type u_1} [TopologicalSpace α] {K : Set α} (hK : IsCompact K) : IsCompact {L : NonemptyCompacts α | ↑L ⊆ K}

theorem TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompact {α : Type u_1} [TopologicalSpace α] {S : Set (NonemptyCompacts α)} (hs : IsCompact S) : IsCompact (⋃ K ∈ S, ↑K)

@[simp]

theorem TopologicalSpace.NonemptyCompacts.compactSpace_iff {α : Type u_1} [TopologicalSpace α] : CompactSpace (NonemptyCompacts α) ↔ CompactSpace α

@[simp]

theorem TopologicalSpace.NonemptyCompacts.noncompactSpace_iff {α : Type u_1} [TopologicalSpace α] : NoncompactSpace (NonemptyCompacts α) ↔ NoncompactSpace α

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