init_add_tail — Mathlib

English

For any Witt vector x and any n, the sum of the initial part init(n)(x) and the tail tail(n)(x) equals x.

Русский

Для любого Witt-вектора x и любого n сумма начальной части init(n)(x) и хвоста tail(n)(x) даёт x.

LaTeX

$$$$\operatorname{init}_n x + \operatorname{tail}_n x = x.$$$$

Lean4

@[simp]
theorem init_add_tail (x : 𝕎 R) (n : ℕ) : init n x + tail n x = x := by
  simp only [init, tail, ← not_lt, select_add_select_not]

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