add_sub_single_one

Mathlib.Data.Finsupp.Order

URI: https://scilib.ai/kg/mathlib#Finsupp.add_sub_single_one

← MathLib Explorer

English

For any u and i with u(i) ≠ 0, we have u - single i 1 + single i 1 = u.

Русский

Если u(i) ≠ 0, то u - single i 1 + single i 1 = u.

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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