English
Changing the index types of a line via three equivalences eη,eα,eι yields a new line with the index function given by applying the map of the equivalences to the original index function.
Русский
Замена типов индексов линии через эквиваленции eη,eα,eι порождает новую линию; её функция индексов задаётся через отображение эквиваленций на исходной функции индекса.
LaTeX
$$$(l : Line\\,\\,\\eta\\,\\alpha\\,\\iota)\\ \\mapsto\\ (l.reindex\\ eη\\ eα\\ eι)$ имеет idxFun i = (l.idxFun\\ (eι.symm\\ i)).map\\ eα\\ eη.$$$
Lean4
/-- Change the index types of a subspace. -/
def reindex (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') : Subspace η' α' ι'
where
idxFun i := (l.idxFun <| eι.symm i).map eα eη
proper
e := (eι.exists_congr fun i ↦ by cases h : idxFun l i <;> simp [*, Equiv.eq_symm_apply]).1 <| l.proper <| eη.symm e
