Theorems · Theorem · general topology

TopologicalSpace.isTopologicalBasis_of_cover

∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} {U : ι → Set α},
  (∀ (i : ι), IsOpen (U i)) →
    ⋃ i, U i = Set.univ →
      ∀ {b : (i : ι) → Set (Set ↑(U i))},
        (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (b i)) →
          TopologicalSpace.IsTopologicalBasis (⋃ i, Set.image Subtype.val '' b i)

Defined in: Mathlib.Topology.Bases
Cited by: 2 results in Mathlib
Foundations: Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.Elemstatement and proof · cited by 7,166
Set.imagestatement and proof · cited by 5,609
Set.preimageproof · cited by 4,946
Set.univstatement and proof · cited by 3,945
Set.iUnionstatement and proof · cited by 2,483
IsOpenstatement and proof · cited by 2,400
Set.mem_image_of_memproof · cited by 371
Set.mem_iUnionproof · cited by 212
Set.image_subset_iffproof · cited by 203
continuous_subtype_valproof · cited by 159

Cited by2

Results whose statement or proof uses this declaration.

TopologicalSpace.IsOpenCover.isTopologicalBasisproof · cited by 1
TopologicalSpace.secondCountableTopology_of_countable_coverproof · cited by 1