English
For x ∈ M and i ∈ ι with h: b i = bi, the representation after reindexing satisfies b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i.
Русский
Пусть для данного i в индексе ι выбрано bi и bi = b i. Тогда после переиндексации координаты удовлетворяют b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i.
LaTeX
$$$\\forall x \\in M, \\forall i \\in ι, \\; b i = bi \\Rightarrow b.\\mathrm{reindexRange}.repr(x)\\langle bi, \\langle i, h\\rangle\\rangle = b.\\mathrm{repr}(x)i.$$$
Lean4
theorem reindexRange_repr' (x : M) {bi : M} {i : ι} (h : b i = bi) : b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i :=
by
nontriviality
subst h
apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm
· intro x y
ext i
simp only [Pi.add_apply, LinearEquiv.map_add, Finsupp.coe_add]
· intro c x
ext i
simp only [Pi.smul_apply, LinearEquiv.map_smul, Finsupp.coe_smul]
· intro i
ext j
simp only [reindexRange_repr_self]
apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))
exact fun i j h => b.injective (Subtype.mk.inj h)
