basis_repr — Mathlib

English

For any x in the product space and any index ji = (j,i), the ji-th coordinate of x with respect to the Pi.basis s is exactly the i-th coordinate of the j-th component x_j with respect to the basis s_j.

Русский

Для любого элемента x в произведении и каждого индекса ji = (j,i) ji-ая координата x по базису Pi.basis s равна i-му координату j-й компоненте x_j по базису s_j.

LaTeX

$$$(\Pi\text{-basis } s).repr\ x\ ji = (s ji.1).repr\ (x ji.1)\ ji.2$$$

Lean4

@[simp]
theorem basis_repr (s : ∀ j, Basis (ιs j) R (Ms j)) (x) (ji) : (Pi.basis s).repr x ji = (s ji.1).repr (x ji.1) ji.2 :=
  rfl

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