Theorems · Theorem · general topology

IsTopologicalBasis.iInf

∀ {β : Type u_1} {ι : Type u_2} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)},
  (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) →
    TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Defined in

Mathlib.Topology.Bases

Cited by

1 results in Mathlib

Foundations

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