sub_add_single_one_cancel — Mathlib

English

For naturals with u i ≠ 0, u - single i 1 + single i 1 = u holds (cancellation).

Русский

Для натуральных чисел с u i ≠ 0, выполняется u - single i 1 + single i 1 = u (раскодирование).

LaTeX

$$$ u \\;\\text{— FinSupp Nat} \\Rightarrow u - \\mathrm{single}(i,1) + \\mathrm{single}(i,1) = u $$$

Lean4

theorem sub_add_single_one_cancel {u : ι →₀ ℕ} {i : ι} (h : u i ≠ 0) : u - single i 1 + single i 1 = u := by
  rw [sub_single_one_add h, add_tsub_cancel_right]

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