instFunLike — Mathlib

English

For an equivalence e: ι' ≃ ι and a scalar v, applying the left piLp congruence to the i'-th coordinate vector yields the i-th coordinate vector corresponding to e(i').

Русский

Для эквивалентности e: ι' ≃ ι и скаляра v применение слева от piLpCongrLeft к единичному вектоpу i' даёт единичный вектор с индексом e(i').

LaTeX

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

Lean4

/-- `b i` is the `i`th basis vector. -/
instance instFunLike : FunLike (OrthonormalBasis ι 𝕜 E) ι E
    where
  coe b i := by classical exact b.repr.symm (EuclideanSpace.single i (1 : 𝕜))
  coe_injective' b b'
    h :=
    repr_injective <|
      LinearIsometryEquiv.toLinearEquiv_injective <|
        LinearEquiv.symm_bijective.injective <|
          LinearEquiv.toLinearMap_injective <| by
            classical
            rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
            simp only
            refine LinearMap.pi_ext fun i k => ?_
            have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
            rw [this, Pi.single_smul]
            replace h := congr_fun h i
            simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
              WithLp.linearEquiv_symm_apply, EuclideanSpace.toLp_single,
              LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
            rw [h]

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