inner_basisFun_real

Mathlib.Analysis.InnerProductSpace.PiL2

URI: https://scilib.ai/kg/mathlib#EuclideanSpace.inner_basisFun_real

English

Applying reindex e to b and evaluating at i' gives b at e.symm(i').

Русский

Применение переиндексации e к b и вычисление в i' равно b по i = e.symm(i').

LaTeX

$$$$ (b.reindex e)(i') = b(e^{-1}(i')). $$$$

Lean4

@[simp]
theorem inner_basisFun_real (x : EuclideanSpace ℝ ι) (i : ι) : inner ℝ x (basisFun ι ℝ i) = x i := by
  rw [real_inner_comm, basisFun_inner]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru