mulSupport_one_add'

Mathlib.Algebra.GroupWithZero.Indicator

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

English

Same as One-add Support, expressed for a function shifted by 1.

Русский

То же самое, что и 'One-add Support', но для функции вида f + 1.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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