Theorems · Definition · general topology

Fin.appendIsometryOfEq

{α : Type u} → [inst : PseudoEMetricSpace α] → {n m l : ℕ} → m + l = n → (Fin m → α) × (Fin l → α) ≃ᵢ (Fin n → α)

The natural IsometryEquiv (Fin m → ℝ) × (Fin l → ℝ) ≃ᵢ (Fin n → ℝ) when m + l = n.

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

2 results in Mathlib

Foundations

Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace