English
Let s be an affine simplex, e an equivalence between finite index sets, and f an injective affine map. Then applying the affine map and then reindexing is the same as reindexing first and then applying the map.
Русский
Пусть s является аффинальным симплексом, e — биекция между конечными множествами индексов, а f — инъективное аффинное отображение. Тогда применение отображения и последующая переиндексация эквивалентны сначала переиндексации, затем применению отображения.
LaTeX
$$$ (s\mapsto f)_{hf}^{\mathrm{reindex}\ e} = (s^{\mathrm{reindex}\ e})_{\mathrm{map}\ f\ hf}$$$
Lean4
theorem reindex_map {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (f : P →ᵃ[k] P₂)
(hf : Function.Injective f) : (s.map f hf).reindex e = (s.reindex e).map f hf :=
rfl
