Theorems · Theorem · general topology

IsUltraUniformity.mk_of_hasBasis

∀ {X : Type u_1} [inst : UniformSpace X] {ι : Type u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s → (∀ (i : ι), p i → (s i).IsSymm) → (∀ (i : ι), p i → (s i).IsTrans) → IsUltraUniformity X

Defined in

Mathlib.Topology.UniformSpace.Ultra.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace