Ultrametric (nonarchimedean) uniform spaces

Ultrametric (nonarchimedean) uniform spaces are ones that generalize ultrametric spaces by having a uniformity based on equivalence relations.

Main definitions

In this file we define IsUltraUniformity, a Prop mixin typeclass.

Main results

• TopologicalSpace.isTopologicalBasis_clopens: a uniform space with a nonarchimedean uniformity has a topological basis of clopen sets in the topology, meaning that it is topologically zero-dimensional.

Implementation notes

As in the Mathlib/Topology/UniformSpace/Defs.lean file, we do not reuse Mathlib/Data/Rel.lean but rather extend the relation properties as needed.

TODOs

• Prove that IsUltraUniformity iff metrizable by IsUltrametricDist on a PseudoMetricSpace under a countable system/basis condition
• Generalize IsUltrametricDist to IsUltrametricUniformity
• Provide IsUltraUniformity for the uniformity in a Valued ring
• Generalize results about open/closed balls and spheres in IsUltraUniformity to combine applications for MetricSpace.ball and valued "balls"
• Use IsUltraUniformity to work with profinite/totally separated spaces

References

• [D. Windisch, Equivalent characterizations of non-Archimedean uniform spaces][windisch2021]
• [A. C. M. van Rooij, Non-Archimedean uniformities][vanrooij1970]

@[deprecated SetRel.IsTrans (since := "2025-10-17")]

def IsTransitiveRel {X : Type u_1} (V : SetRel X X) : Prop

The relation is transitive.

@[deprecated SetRel.comp_subset_self (since := "2025-10-17")]

theorem IsTransitiveRel.comp_subset_self {X : Type u_1} {s : SetRel X X} (h : IsTransitiveRel s) : s.comp s ⊆ s

@[deprecated SetRel.isTrans_iff_comp_subset_self (since := "2025-10-17")]

theorem isTransitiveRel_iff_comp_subset_self {X : Type u_1} {s : SetRel X X} : IsTransitiveRel s ↔ s.comp s ⊆ s

@[deprecated SetRel.isTrans_empty (since := "2025-10-17")]

theorem isTransitiveRel_empty {X : Type u_1} : IsTransitiveRel ∅

@[deprecated SetRel.isTrans_univ (since := "2025-10-17")]

theorem isTransitiveRel_univ {X : Type u_1} : IsTransitiveRel Set.univ

@[deprecated SetRel.isTrans_singleton (since := "2025-10-17")]

theorem isTransitiveRel_singleton {X : Type u_1} (x y : X) : IsTransitiveRel {(x, y)}

@[deprecated SetRel.isTrans_inter (since := "2025-10-17")]

theorem IsTransitiveRel.inter {X : Type u_1} {s t : SetRel X X} (hs : IsTransitiveRel s) (ht : IsTransitiveRel t) : IsTransitiveRel (s ∩ t)

@[deprecated SetRel.isTrans_iInter (since := "2025-10-17")]

theorem IsTransitiveRel.iInter {X : Type u_1} {ι : Type u_2} {U : ι → SetRel X X} (hU : ∀ (i : ι), IsTransitiveRel (U i)) : IsTransitiveRel (⋂ (i : ι), U i)

@[deprecated SetRel.IsTrans.sInter (since := "2025-10-17")]

theorem IsTransitiveRel.sInter {X : Type u_1} {s : Set (SetRel X X)} (h : ∀ i ∈ s, IsTransitiveRel i) : IsTransitiveRel (⋂₀ s)

@[deprecated SetRel.isTrans_preimage (since := "2025-10-17")]

theorem IsTransitiveRel.preimage_prodMap {X : Type u_1} {Y : Type u_2} {t : Set (Y × Y)} (ht : IsTransitiveRel t) (f : X → Y) : IsTransitiveRel (Prod.map f f ⁻¹' t)

@[deprecated SetRel.isTrans_symmetrize (since := "2025-10-17")]

theorem IsTransitiveRel.symmetrizeRel {X : Type u_1} {s : SetRel X X} (h : IsTransitiveRel s) : IsTransitiveRel s.symmetrize

@[deprecated SetRel.comp_eq_self (since := "2025-10-17")]

theorem IsTransitiveRel.comp_eq_of_idRel_subset {X : Type u_1} {s : SetRel X X} (h : IsTransitiveRel s) (h' : idRel ⊆ s) : s.comp s = s

theorem IsTransitiveRel.prod_subset_trans {X : Type u_1} {s : SetRel X X} {t u v : Set X} [s.IsTrans] (htu : t ×ˢ u ⊆ s) (huv : u ×ˢ v ⊆ s) (hu : u.Nonempty) : t ×ˢ v ⊆ s

theorem IsTransitiveRel.mem_filter_prod_trans {X : Type u_1} {s : SetRel X X} {f g h : Filter X} [g.NeBot] [s.IsTrans] (hfg : s ∈ f ×ˢ g) (hgh : s ∈ g ×ˢ h) : s ∈ f ×ˢ h

@[deprecated IsTransitiveRel.mem_filter_prod_trans (since := "2025-10-08")]

theorem IsTransitiveRel.mem_filter_prod_comm {X : Type u_1} {s : SetRel X X} {f g h : Filter X} [g.NeBot] [s.IsTrans] (hfg : s ∈ f ×ˢ g) (hgh : s ∈ g ×ˢ h) : s ∈ f ×ˢ h

Alias of IsTransitiveRel.mem_filter_prod_trans.

theorem ball_subset_of_mem {X : Type u_1} {V : SetRel X X} [V.IsTrans] {x y : X} (hy : y ∈ UniformSpace.ball x V) : UniformSpace.ball y V ⊆ UniformSpace.ball x V

theorem ball_eq_of_mem {X : Type u_1} {V : SetRel X X} [V.IsSymm] [V.IsTrans] {x y : X} (hy : y ∈ UniformSpace.ball x V) : UniformSpace.ball x V = UniformSpace.ball y V

class IsUltraUniformity (X : Type u_1) [UniformSpace X] : Prop

A uniform space is ultrametric if the uniformity 𝓤 X has a basis of equivalence relations.

• hasBasis : (uniformity X).HasBasis (fun (s : SetRel X X) => s ∈ uniformity X ∧ s.IsSymm ∧ s.IsTrans) id

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

theorem IsUltraUniformity.mem_nhds_iff_symm_trans {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] {x : X} {s : Set X} : s ∈ nhds x ↔ ∃ V ∈ uniformity X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ UniformSpace.ball x V ⊆ s

theorem UniformSpace.isOpen_ball_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsTrans] (h' : V ∈ uniformity X) : IsOpen (ball x V)

theorem UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans] (h' : V ∈ uniformity X) : IsClosed (ball x V)

@[deprecated UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity (since := "2025-10-17")]

theorem UniformSpace.isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans] (h' : V ∈ uniformity X) : IsClosed (ball x V)

Alias of UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity.

theorem UniformSpace.isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans] (h' : V ∈ uniformity X) : IsClopen (ball x V)

theorem UniformSpace.nhds_basis_clopens {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsClopen s) id

theorem TopologicalSpace.isTopologicalBasis_clopens {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : IsTopologicalBasis {s : Set X | IsClopen s}

A uniform space with a nonarchimedean uniformity is zero-dimensional.