equivFunL_symm_apply_repr — Mathlib

English

Let v be a finite basis of E; the map sending e ∈ E to its coordinate function v.equivFun e: ι → 𝕜 is a continuous linear equivalence E ≃L[𝕜] (ι → 𝕜). The inverse recovers e from its coordinates.

Русский

Пусть v — конечный базис пространства E; отображение e ↦ координатная функция v.equivFun e: ι → 𝕜 образует непрерывно линейное эквивалентное отображение E ≃L[𝕜] (ι → 𝕜). Обратная карта восстанавливает элемент из координат.

LaTeX

$$$E \\simeq_L[𝕜] (ι \\to 𝕜)$$$

Lean4

@[simp]
theorem equivFunL_symm_apply_repr (v : Basis ι 𝕜 E) (x : E) : v.equivFunL.symm (v.repr x) = x :=
  v.equivFunL.symm_apply_apply x

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