neLocus_self_sub_left

Mathlib.Data.DFinsupp.NeLocus

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

English

The neLocus of f − g with respect to f equals g.support: neLocus (f − g) f = g.support.

Русский

Локус вычитания слева равен опоре g.

LaTeX

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

Lean4

@[simp]
theorem neLocus_self_sub_left : neLocus (f - g) f = g.support := by rw [neLocus_comm, neLocus_self_sub_right]

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

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

Разделы

Аффилиация

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