linearEquivTuple_symm_apply — Mathlib

English

The inverse of the linear equivalence tensorial tuple acts by sending x ∈ Fin 2 → R to the pair (x(0), x(1)).

Русский

Обратное линейное эквивалентное отображение tuple отправляет x ∈ Fin 2 → R в пару (x(0), x(1)).

LaTeX

$$$(\\text{linearEquivTuple } a b)^{-1} x = \\langle x_0, x_1 \\rangle$ for $x : \\mathrm{Fin}^2 \\to R$$$

Lean4

@[simp]
theorem linearEquivTuple_symm_apply (x : Fin 2 → R) : (linearEquivTuple a b).symm x = ⟨x 0, x 1⟩ :=
  rfl

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