Theorems · Theorem · general topology

TopologicalSpace.IsTopologicalBasis.nonemptyCompacts

∀ {α : Type u_1} [inst : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    TopologicalSpace.IsTopologicalBasis
      ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | 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.

Defined in

Mathlib.Topology.Sets.VietorisTopology

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace