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

theorem IsSymmetricRel.cauchyFilter_gen {X : Type u_1} [UniformSpace X] {s : Set (X × X)} (h : IsSymmetricRel s) : IsSymmetricRel (CauchyFilter.gen s)

theorem IsTransitiveRel.cauchyFilter_gen {X : Type u_1} [UniformSpace X] {s : Set (X × X)} (hs : IsTransitiveRel s) : IsTransitiveRel (CauchyFilter.gen s)

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)