support_conjneg

Mathlib.Algebra.Star.Conjneg

URI: https://scilib.ai/kg/mathlib#support_conjneg

English

The support of conjneg f equals the negation of the support of f.

Русский

Поддержка conjneg f равна −поддержке f.

LaTeX

$$$\operatorname{supp}(\operatorname{conjneg} f) = -\operatorname{supp}(f)$$$

Lean4

@[simp]
theorem support_conjneg (f : G → R) : support (conjneg f) = -support f := by ext; simp [starRingEnd_apply]

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

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

Разделы

Аффилиация

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