Ultrametric spaces

This file defines ultrametric spaces, implemented as a mixin on the Dist, so that it can apply on pseudometric spaces as well.

Main definitions

• IsUltrametricDist X: Annotates dist : X → X → ℝ as respecting the ultrametric inequality of dist(x, z) ≤ max {dist(x,y), dist(y,z)}

Implementation details

The mixin could have been defined as a hypothesis to be carried around, instead of relying on typeclass synthesis. However, since we declare a (pseudo)metric space on a type using typeclass arguments, one can declare the ultrametricity at the same time. For example, one could say [Norm K] [Fact (IsNonarchimedean (norm : K → ℝ))],

The file imports a later file in the hierarchy of pseudometric spaces, since Metric.isClosed_ball and Metric.isClosed_sphere is proven in a later file using more conceptual results.

TODO: Generalize to ultrametric uniformities

Tags

ultrametric, nonarchimedean

class IsUltrametricDist (X : Type u_2) [Dist X] : Prop

The dist : X → X → ℝ respects the ultrametric inequality of dist(x, z) ≤ max (dist(x,y)) (dist(y,z)).

• dist_triangle_max (x y z : X) : dist x z ≤ dist x y ⊔ dist y z

theorem dist_triangle_max {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y z : X) : dist x z ≤ dist x y ⊔ dist y z

theorem IsUltrametricDist.dist_eq_max_of_dist_ne_dist {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y z : X) (h : dist x y ≠ dist y z) : dist x z = dist x y ⊔ dist y z

All triangles are isosceles in an ultrametric space.

instance IsUltrametricDist.subtype {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (p : X → Prop) : IsUltrametricDist (Subtype p)

theorem IsUltrametricDist.ball_eq_of_mem {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ} (h : y ∈ Metric.ball x r) : Metric.ball x r = Metric.ball y r

theorem IsUltrametricDist.mem_ball_iff {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ} : y ∈ Metric.ball x r ↔ x ∈ Metric.ball y r

theorem IsUltrametricDist.ball_subset_trichotomy {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r s : ℝ) : Metric.ball x r ⊆ Metric.ball y s ∨ Metric.ball y s ⊆ Metric.ball x r ∨ Disjoint (Metric.ball x r) (Metric.ball y s)

theorem IsUltrametricDist.ball_eq_or_disjoint {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r : ℝ) : Metric.ball x r = Metric.ball y r ∨ Disjoint (Metric.ball x r) (Metric.ball y r)

theorem IsUltrametricDist.closedBall_eq_of_mem {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ} (h : y ∈ Metric.closedBall x r) : Metric.closedBall x r = Metric.closedBall y r

theorem IsUltrametricDist.mem_closedBall_iff {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ} : y ∈ Metric.closedBall x r ↔ x ∈ Metric.closedBall y r

theorem IsUltrametricDist.closedBall_subset_trichotomy {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r s : ℝ) : Metric.closedBall x r ⊆ Metric.closedBall y s ∨ Metric.closedBall y s ⊆ Metric.closedBall x r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y s)

theorem IsUltrametricDist.isClosed_ball {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ) : IsClosed (Metric.ball x r)

theorem IsUltrametricDist.isClopen_ball {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ) : IsClopen (Metric.ball x r)

theorem IsUltrametricDist.frontier_ball_eq_empty {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ) : frontier (Metric.ball x r) = ∅

theorem IsUltrametricDist.closedBall_eq_or_disjoint {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r : ℝ) : Metric.closedBall x r = Metric.closedBall y r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y r)

theorem IsUltrametricDist.isOpen_closedBall {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsOpen (Metric.closedBall x r)

theorem IsUltrametricDist.isClopen_closedBall {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsClopen (Metric.closedBall x r)

theorem IsUltrametricDist.frontier_closedBall_eq_empty {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.closedBall x r) = ∅

theorem IsUltrametricDist.isOpen_sphere {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsOpen (Metric.sphere x r)

theorem IsUltrametricDist.isClopen_sphere {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsClopen (Metric.sphere x r)