neLocus_neg_neg

Mathlib.Data.Finsupp.NeLocus

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

English

The not-equal locus is preserved under pointwise negation: neLocus(-f)(-g) = f.neLocus(g).

Русский

Локус различий сохраняется при поэлементном отрицании: neLocus(-f)(-g) = f.neLocus(g).

LaTeX

$$$ neLocus (-f) (-g) = f.neLocus g $$$

Lean4

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

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

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

Разделы

Аффилиация

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