An unrestricted Kuratowski injectivity coordinate

The paper uses the bounded distance-difference function on the metric quotient. Here the same functions are represented in ℓ∞(P, ℝ), indexed by every point of P. Unlike Mathlib's countable Kuratowski embedding, this construction does not require separability.

noncomputable def ScottishBook155.fullKuratowski {P : Type u} [MetricSpace P] (base z : P) : ↥(lp (fun (x : P) => ℝ) ⊤)

The distance-difference Kuratowski coordinate based at base.

Equations

• ScottishBook155.fullKuratowski base z = ⟨fun (u : P) => dist z u - dist base u, ⋯⟩

theorem ScottishBook155.fullKuratowski_apply {P : Type u} [MetricSpace P] (base z u : P) : ↑(fullKuratowski base z) u = dist z u - dist base u

theorem ScottishBook155.fullKuratowski_base {P : Type u} [MetricSpace P] (base : P) : fullKuratowski base base = 0

theorem ScottishBook155.fullKuratowski_dist_le {P : Type u} [MetricSpace P] (base z w : P) : dist (fullKuratowski base z) (fullKuratowski base w) ≤ dist z w

theorem ScottishBook155.fullKuratowski_isometry {P : Type u} [MetricSpace P] (base : P) : Isometry (fullKuratowski base)

The unrestricted distance-difference coordinate is an isometry.

theorem ScottishBook155.fullKuratowski_injective {P : Type u} [MetricSpace P] (base : P) : Function.Injective (fullKuratowski base)