neLocus_neg_neg

Mathlib.Data.DFinsupp.NeLocus

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

English

Negating both f and g does not change the neLocus: neLocus(-f, -g) = neLocus(f, g).

Русский

Отрицание обеих функций не изменяет локус различий.

LaTeX

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

Lean4

@[simp]
theorem neLocus_neg_neg : neLocus (-f) (-g) = f.neLocus g :=
  mapRange_neLocus_eq _ _ (fun _a ↦ neg_zero) fun _a ↦ neg_injective

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

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

Разделы

Аффилиация

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