English
If n = m + l, there is an isometry between (Fin m → α) × (Fin l → α) and Fin n → α given by composing Fin.appendIsometry m l with piCongrLeft (finCongr hmln).
Русский
Если n = m + l, существует изометрия между (Fin m → α) × (Fin l → α) и Fin n → α, заданная композицией Fin.appendIsometry m l и piCongrLeft (finCongr hmln).
LaTeX
$$$ (m,l,n)\ (hmln: m+l=n) : (Fin m \to α) \times (Fin l \to α) \simeq_i (Fin n \to α) $$$
Lean4
/-- The natural `IsometryEquiv` `(Fin m → ℝ) × (Fin l → ℝ) ≃ᵢ (Fin n → ℝ)` when `m + l = n`. -/
@[simps!]
def _root_.Fin.appendIsometryOfEq {n m l : ℕ} (hmln : m + l = n) : (Fin m → α) × (Fin l → α) ≃ᵢ (Fin n → α) :=
(Fin.appendIsometry m l).trans (IsometryEquiv.piCongrLeft (Y := fun _ ↦ α) (finCongr hmln))
