Theorems · Theorem · general topology

CompleteSpace.iInf

∀ {ι : Type u_4} {X : Type u_5} {u : ι → UniformSpace X},
  (∀ (i : ι), CompleteSpace X) → (∃ t, T2Space X ∧ ∀ (i : ι), (u i).toTopologicalSpace ≤ t) → CompleteSpace X

An infimum of complete uniformities is complete, as long as the whole family is bounded by some common T2 topology.

Defined in

Mathlib.Topology.UniformSpace.Pi

Cited by

1 results in Mathlib

Foundations

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