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

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

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)