The sup distance over a one-point index type

For a product of pseudometric spaces over a one-point index type, the sup distance is the distance of the only coordinates (Pi.dist_unique), so balls, closed balls and spheres are detected on that coordinate (Pi.mem_ball_unique, Pi.mem_closedBall_unique and Pi.mem_sphere_unique), and balls and closed balls are preimages under evaluation at that coordinate (Pi.ball_unique and Pi.closedBall_unique). This is the pointwise form of IsometryEquiv.funUnique, stated for dependent families.

@[simp]

theorem Pi.dist_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] (f g : (i : ι) → X i) : dist f g = dist (f default) (g default)

Over a one-point index type, the sup distance is the distance of the only coordinates.

theorem Pi.mem_ball_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] {f g : (i : ι) → X i} {r : ℝ} : f ∈ Metric.ball g r ↔ f default ∈ Metric.ball (g default) r

Over a one-point index type, a ball is the ball around the only coordinate.

theorem Pi.mem_closedBall_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] {f g : (i : ι) → X i} {r : ℝ} : f ∈ Metric.closedBall g r ↔ f default ∈ Metric.closedBall (g default) r

Over a one-point index type, a closed ball is the closed ball around the only coordinate.

theorem Pi.ball_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] (g : (i : ι) → X i) (r : ℝ) : Metric.ball g r = Function.eval default ⁻¹' Metric.ball (g default) r

Over a one-point index type, a ball is the preimage under evaluation of the ball around the only coordinate.

theorem Pi.closedBall_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] (g : (i : ι) → X i) (r : ℝ) : Metric.closedBall g r = Function.eval default ⁻¹' Metric.closedBall (g default) r

Over a one-point index type, a closed ball is the preimage under evaluation of the closed ball around the only coordinate.

theorem Pi.mem_sphere_unique {ι : Type u_1} {X : ι → Type u_2} [Fintype ι] [Unique ι] [(i : ι) → PseudoMetricSpace (X i)] {f g : (i : ι) → X i} {r : ℝ} : f ∈ Metric.sphere g r ↔ f default ∈ Metric.sphere (g default) r

Over a one-point index type, a sphere is the sphere around the only coordinate.