Theorems · Theorem · general topology

CompletePseudometrizable.iInf

∀ {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ι → TopologicalSpace α},
  (∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀) →
    (∀ (i : ι), ∃ u, CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = t i) →
      ∃ u, CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i

Defined in

Mathlib.Topology.MetricSpace.Polish

Cited by

1 results in Mathlib

Foundations

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

Assumes

Countable