sub_single_one_add — Mathlib

English

If u(a) ≠ 0, then u - single a 1 + u' = u + u' - single a 1; i.e., moving one unit from the a-component to the rest preserves the total when you later add u'.

Русский

Если u(a) ≠ 0, то u - single a 1 + u' = u + u' - single a 1; то есть перенос единицы из компоненты a сохраняет общую величину после сложения u'.

LaTeX

$$$ u - \\mathrm{single}(a,1) + u' = u + u' - \\mathrm{single}(a,1) $$$

Lean4

theorem sub_single_one_add {a : ι} {u u' : ι →₀ ℕ} (h : u a ≠ 0) : u - single a 1 + u' = u + u' - single a 1 :=
  tsub_add_eq_add_tsub <| single_le_iff.mpr <| Nat.one_le_iff_ne_zero.mpr h

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