Completions of ultrametric (nonarchimedean) uniform spaces

Main results

• IsUltraUniformity.completion_iff: a Hausdorff completion has a nonarchimedean uniformity iff the underlying space has a nonarchimedean uniformity.

theorem IsUniformInducing.isUltraUniformity {X : Type u_1} {Y : Type u_2} [UniformSpace X] [UniformSpace Y] [IsUltraUniformity Y] {f : X → Y} (hf : IsUniformInducing f) : IsUltraUniformity X

instance CauchyFilter.isSymm_gen {X : Type u_1} [UniformSpace X] {s : SetRel X X} [s.IsSymm] : (gen s).IsSymm

@[deprecated CauchyFilter.isSymm_gen (since := "2025-10-17")]

theorem IsSymmetricRel.cauchyFilter_gen {X : Type u_1} [UniformSpace X] {s : SetRel X X} [s.IsSymm] : (CauchyFilter.gen s).IsSymm

Alias of CauchyFilter.isSymm_gen.

instance CauchyFilter.isTrans_gen {X : Type u_1} [UniformSpace X] {s : SetRel X X} [s.IsTrans] : (gen s).IsTrans

@[deprecated CauchyFilter.isTrans_gen (since := "2025-10-17")]

theorem IsTransitiveRel.cauchyFilter_gen {X : Type u_1} [UniformSpace X] {s : SetRel X X} [s.IsTrans] : (CauchyFilter.gen s).IsTrans

Alias of CauchyFilter.isTrans_gen.

instance IsUltraUniformity.cauchyFilter {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : IsUltraUniformity (CauchyFilter X)

@[simp]

theorem IsUltraUniformity.cauchyFilter_iff {X : Type u_1} [UniformSpace X] : IsUltraUniformity (CauchyFilter X) ↔ IsUltraUniformity X

instance IsUltraUniformity.separationQuotient {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : IsUltraUniformity (SeparationQuotient X)

@[simp]

theorem IsUltraUniformity.separationQuotient_iff {X : Type u_1} [UniformSpace X] : IsUltraUniformity (SeparationQuotient X) ↔ IsUltraUniformity X

@[simp]

theorem IsUltraUniformity.completion_iff {X : Type u_1} [UniformSpace X] : IsUltraUniformity (UniformSpace.Completion X) ↔ IsUltraUniformity X

instance IsUltraUniformity.completion {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : IsUltraUniformity (UniformSpace.Completion X)