Documentation

TauCeti.Topology.MetricSpace.Isometry.Basic

Splitting off the last coordinate of a tuple is an isometry #

For a pseudo-emetric space α, the identification Fin.initLastIsometry α n of Fin (n + 1) → α with (Fin n → α) × α, sending x to (Fin.init x, x (Fin.last n)), is an isometry for the sup distances. It is Fin.appendIsometry n 1 read backwards, with the second factor Fin 1 → α identified with α.

So it carries balls, closed balls and spheres around the origin onto the corresponding products: a ball onto the product of balls, and a sphere onto the union of sphere ×ˢ closedBall and closedBall ×ˢ sphere. This is how the characteristic map of a cell of a product with an interval splits off the interval coordinate.

Main declarations #

source
def Fin.initLastIsometry (α : Type u_1) [PseudoEMetricSpace α] (n : ℕ) :
(Fin (n + 1) → α) ≃ᵢ (Fin n → α) × α

The identification of Fin (n + 1) → α with (Fin n → α) × α, splitting off the last coordinate; it is an isometry for the sup distances.

Instances For
    source
    @[simp]
    theorem Fin.initLastIsometry_apply {α : Type u_1} [PseudoEMetricSpace α] {n : ℕ} (x : Fin (n + 1) → α) :
    (initLastIsometry α n) x = (init x, x (last n))

    Splitting off the last coordinate sends x to (Fin.init x, x (Fin.last n)).

    source
    @[simp]
    theorem Fin.initLastIsometry_symm_apply {α : Type u_1} [PseudoEMetricSpace α] {n : ℕ} (p : (Fin n → α) × α) :
    (initLastIsometry α n).symm p = snoc p.1 p.2

    The inverse of splitting off the last coordinate appends the second component with Fin.snoc.

    source
    theorem Fin.initLastIsometry_zero {α : Type u_1} [PseudoEMetricSpace α] [Zero α] (n : ℕ) :
    (initLastIsometry α n) 0 = 0

    Splitting off the last coordinate sends the origin to the origin.

    source
    theorem Fin.image_ball_initLastIsometry {α : Type u_1} [PseudoMetricSpace α] [Zero α] (n : ℕ) (r : ℝ) :
    ⇑(initLastIsometry α n) '' Metric.ball 0 r = Metric.ball 0 r ×ˢ Metric.ball 0 r

    Splitting off the last coordinate carries the ball of radius r around the origin onto the product of the balls of radius r around the origin.

    source
    theorem Fin.image_closedBall_initLastIsometry {α : Type u_1} [PseudoMetricSpace α] [Zero α] (n : ℕ) (r : ℝ) :
    ⇑(initLastIsometry α n) '' Metric.closedBall 0 r = Metric.closedBall 0 r ×ˢ Metric.closedBall 0 r

    Splitting off the last coordinate carries the closed ball of radius r around the origin onto the product of the closed balls of radius r around the origin.

    source
    theorem Fin.image_sphere_initLastIsometry {α : Type u_1} [PseudoMetricSpace α] [Zero α] (n : ℕ) (r : ℝ) :
    ⇑(initLastIsometry α n) '' Metric.sphere 0 r = Metric.sphere 0 r ×ˢ Metric.closedBall 0 r ∪ Metric.closedBall 0 r ×ˢ Metric.sphere 0 r

    Splitting off the last coordinate carries the sphere of radius r around the origin onto the union of sphere ×ˢ closedBall and closedBall ×ˢ sphere of radius r around the origin.

    source
    theorem Fin.preimage_ball_prod_initLastIsometry {α : Type u_1} [PseudoMetricSpace α] [Zero α] (n : ℕ) (r : ℝ) :
    ⇑(initLastIsometry α n) ⁻¹' Metric.ball 0 r ×ˢ Metric.ball 0 r = Metric.ball 0 r

    The preimage under splitting off the last coordinate of the product of the balls of radius r around the origin is the ball of radius r around the origin.