removeNth — Mathlib

English

RemoveNth(p, f) is the tuple obtained by removing the p-th entry of the tuple f: Fin(n+1) → α. It is the function on Fin n given by i ↦ f(p.succAbove(i)).

Русский

RemoveNth(p, f) — это кортеж, полученный из кортежа f: Fin(n+1) → α путем удаления p-й позиции. Это функция на Fin n, заданная i ↦ f(p.succAbove(i)).

LaTeX

$$$(removeNth\ p\ f)\ i = f(p.\\succAbove i).$$$

Lean4

/-- Remove the `p`-th entry of a tuple. -/
def removeNth (p : Fin (n + 1)) (f : ∀ i, α i) : ∀ i, α (p.succAbove i) := fun i ↦ f (p.succAbove i)

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