Theorems · Theorem · general topology

TopologicalSpace.IsOpenCover.isTopologicalBasis

∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u →
    ∀ {B : (i : ι) → Set (Set ↥(u i))},
      (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (B i)) →
        TopologicalSpace.IsTopologicalBasis (⋃ i, (fun x => Subtype.val '' x) '' B i)

Defined in

Mathlib.Topology.Sets.OpenCover

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace