mulSupport_add_one'

Mathlib.Algebra.GroupWithZero.Indicator

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_add_one'

English

Same as Add-one Support, for the function f + 1.

Русский

То же самое для функции f + 1.

LaTeX

$$$\\operatorname{mulSupport}(f + 1) = \\operatorname{support}(f)$$$

Lean4

theorem mulSupport_add_one' [AddRightCancelMonoid R] (f : ι → R) : mulSupport (f + 1) = support f :=
  mulSupport_add_one f

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

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

Разделы

Аффилиация

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