insertNth_self_removeNth — Mathlib

English

Reconstructing the original sequence from its p-th element and the remaining tail recovers the original tuple.

Русский

Восстановление исходного кортежа по p-му элементу и оставшемуся хвосту восстанавливает исходный кортеж.

LaTeX

$$$$ \mathrm{insertNth}\ p\ (f\ p)\ (\mathrm{removeNth}\ p\ f) = f $$$$

Lean4

theorem insertNth_self_removeNth (p : Fin (n + 1)) (f : ∀ j, α j) : insertNth p (f p) (removeNth p f) = f := by simp

Похожие утверждения