Theorems · Theorem · general topology

pi_generateFrom_eq_finite

∀ {ι : Type u_5} {X : ι → Type u_9} {g : (a : ι) → Set (Set (X a))} [Finite ι],
  (∀ (a : ι), ⋃₀ g a = Set.univ) →
    Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.univ.pi s}

Defined in

Mathlib.Topology.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite