neLocus_neg

Mathlib.Data.DFinsupp.NeLocus

URI: https://scilib.ai/kg/mathlib#DFinsupp.neLocus_neg

English

Negating one side maps the neLocus to the negated other side: neLocus(-f, g) = f.neLocus(-g).

Русский

При отделении одного аргумента локус преобразуется соответственно.

LaTeX

$$$ \mathrm{neLocus}(-f) g = f.neLocus (-g) $$$

Lean4

theorem neLocus_neg : neLocus (-f) g = f.neLocus (-g) := by rw [← neLocus_neg_neg, neg_neg]

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

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

Разделы

Аффилиация

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