collectedBasis_repr_of_mem — Mathlib

English

The coordinate representation of an element x ∈ M with respect to the collected basis matches the representation given by the bases in each A_i on the corresponding coordinates.

Русский

Координатное представление элемента x ∈ M относительно собранного базиса совпадает с представлением по базам в каждом A_i на соответствующих координатах.

LaTeX

$$$\text{(h.collectedBasis v).repr}(x)_{\langle i,a\rangle} = (v_i).repr(x|_{A_i})_a$$$

Lean4

theorem collectedBasis_repr_of_mem (h : IsInternal A) {α : ι → Type*} (v : ∀ i, Basis (α i) R (A i)) {x : M} {i : ι}
    {a : α i} (hx : x ∈ A i) : (h.collectedBasis v).repr x ⟨i, a⟩ = (v i).repr ⟨x, hx⟩ a :=
  by
  change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
  simp [h.ofBijective_coeLinearMap_of_mem hx]

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