removeNth_apply

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.removeNth_apply

English

For any p and f, and any i, the i-th entry of removeNth p f is f(p.succAbove i).

Русский

Для любых p и f и любого i элемент на позиции i в removeNth p f равен f(p.succAbove i).

LaTeX

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

Lean4

theorem removeNth_apply (p : Fin (n + 1)) (f : ∀ i, α i) (i : Fin n) : p.removeNth f i = f (p.succAbove i) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru