Theorems · Theorem · general topology

TopologicalSpace.NonemptyCompacts.isTopologicalBasis

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

Defined in

Mathlib.Topology.Sets.VietorisTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace