reindex_apply — Mathlib

English

Equivalence of span constructions: span h s equals the span generated by the image of s under v'.

Русский

Эквивалентность конструкций span: один и тот же подпространственный базис порождается образом s под v'.

LaTeX

$$$$ \\mathrm{OrthonormalBasis}.span(h,s) = \\mathrm{OrthonormalBasis}.span'(h,s) $$$$

Lean4

protected theorem reindex_apply (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (i' : ι') :
    (b.reindex e) i' = b (e.symm i') := by
  classical
  dsimp [reindex]
  rw [coe_ofRepr]
  dsimp
  rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm, EuclideanSpace.piLpCongrLeft_single]

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