English
If opα and opβ are binary operations on α and β, f preserves the operation in the sense that f(x opα y) = f x opβ f y, then applying f to the contracted sequence equals contracting the image sequence after applying f.
Русский
Если две бинарные операции opα и opβ совместимы через f таким образом, что f(x opα y) = opβ (f x) (f y), то применение f к сжатой последовательности эквивалентно сжатию образной последовательности после применения f.
LaTeX
$$$\\forall f, j, g, \\; (\\forall x,y, f(x\\ op_α\\ y) = op_β (f x) (f y)) \\rightarrow f \\circ contractNth\ j\\ op_α\\ g = contractNth\\ j\\ op_β\\ (f \\circ g)$$$
Lean4
theorem comp_contractNth {β : Sort*} (opα : α → α → α) (opβ : β → β → β) {f : α → β}
(hf : ∀ x y, f (opα x y) = opβ (f x) (f y)) (j : Fin (n + 1)) (g : Fin (n + 1) → α) :
f ∘ contractNth j opα g = contractNth j opβ (f ∘ g) :=
by
ext x
rcases lt_trichotomy (x : ℕ) j with (h | h | h)
· simp only [Function.comp_apply, contractNth_apply_of_lt, h]
· simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]
· simp only [Function.comp_apply, contractNth_apply_of_gt, h]
