English
For l reindexed by eη,eα,eι and for x: η'→α' and i ∈ ι', the value equals eα applied to the original line evaluated at the composed input: (l.reindex eη eα eι).toFun x i = eα (l.toFun (eα⁻¹ ∘ x ∘ eη) (eι⁻¹ i)).
Русский
Для переиндексированной линии через eη,eα,eι и для x: η'→α' и i∈ι', значение равно применению eα к исходной линии на скомпонованном вводе: (l.reindex eη eα eι).toFun x i = eα (l.toFun (eα⁻¹ ∘ x ∘ eη) (eι⁻¹ i)).
LaTeX
$$$(l.reindex\\ eη\\ eα\\ eι).toFun\\ x\\ i = eα\\left( l.toFun\\left( eα^{-1}\\circ x\\circ eη\\right)\\left( eι^{-1}\\,i\\right)\\right).$$$
Lean4
@[simp]
theorem reindex_apply (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') (x i) :
l.reindex eη eα eι x i = eα (l (eα.symm ∘ x ∘ eη) <| eι.symm i) := by
cases h : l.idxFun (eι.symm i) <;> simp [h, reindex, coe_apply]
