mulSupport_update_one

Mathlib.Algebra.Notation.Support

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_update_one

← MathLib Explorer

English

mulSupport (update f x 1) = mulSupport f \\ { x }.

Русский

mulSupport (обновление f в x до 1) равно mulSupport f без {x}.

LaTeX

$$$ \\mathrm{mulSupport}(\\mathrm{update}\\ f\\ x\\ 1) = \\mathrm{mulSupport}(f) \\setminus \\{ x \\} $$$

Lean4

@[to_additive]
theorem mulSupport_update_one [DecidableEq ι] (f : ι → M) (x : ι) : mulSupport (update f x 1) = mulSupport f \ { x } :=
  by ext a; obtain rfl | hne := eq_or_ne a x <;> simp [*]

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

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

Разделы

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

Аффилиация

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