support_erase

Mathlib.Algebra.SkewMonoidAlgebra.Single

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.support_erase

English

Erasing an index a from the function f reduces the support by erasing a from f’s support.

Русский

Стирание индекса a из функции f уменьшает её поддержку, стирая a из поддержки f.

LaTeX

$$$\operatorname{support}(f.update a) = \operatorname{support}(f) \setminus \{a\}$$$

Lean4

@[simp]
theorem support_erase [DecidableEq α] : (f.erase a).support = f.support.erase a := by ext; simp [erase]

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

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

Разделы

Аффилиация

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