piLpCongrLeft_single — Mathlib

English

Given a bijection e: ι' → ι, mapping a single i' in ι' to the corresponding i = e(i') in ι under the canonical coordinate isometry, the i'-th coordinate vector maps to the i-th coordinate vector.

Русский

Задавая биекция e: ι' → ι, через каноническую изометрическую карту координат, единичный вектор с индексом i' отображается в единичный вектор с индексом e(i').

LaTeX

$$$\text{piLpCongrLeft}_2^{𝕜} (e) (\mathrm{EuclideanSpace}.single i' v) = \mathrm{EuclideanSpace}.single (e i') v$$$

Lean4

theorem piLpCongrLeft_single {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜) :
    LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e (EuclideanSpace.single i' v) = EuclideanSpace.single (e i') v :=
  LinearIsometryEquiv.piLpCongrLeft_single e i' _

Похожие утверждения