repr_apply_apply — Mathlib

English

Under a finite permutation of indices, a single-vector basis element maps to the corresponding permuted basis element in the target index set.

Русский

При применении перестановки индексов к единичному вектору базиса он переходит в соответствующий элемент базиса в целевом наборе индексов.

LaTeX

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

Lean4

protected theorem repr_apply_apply (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι) : b.repr v i = ⟪b i, v⟫ := by
  classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
  simp only [one_mul, map_one]

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