English
Let v,w : Fin n → R and f : Fin n → Fin n. Then substituting f into the inputs of both v and w yields that the Vandermonde projection of (v ∘ f, w ∘ f) equals the submatrix of the Vandermonde projection of (v,w) with indices f and the identity on Fin n.
Русский
Пусть v,w : Fin n → R и f : Fin n → Fin n. Тогда Vandermonde-проекция от (v ∘ f, w ∘ f) равна подматрице Vandermonde-проекции от (v, w) по индексу f и единичной по Fin n.
LaTeX
$$$ \\mathrm{projVandermonde}(v \\circ f)(w \\circ f) = (\\mathrm{projVandermonde}~v~w).\\mathrm{submatrix}~f~\\mathrm{id}. $$$
Lean4
theorem projVandermonde_comp {v w : Fin n → R} (f : Fin n → Fin n) :
projVandermonde (v ∘ f) (w ∘ f) = (projVandermonde v w).submatrix f id :=
rfl
