neLocus_zero_left

Mathlib.Data.DFinsupp.NeLocus

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

English

The right-hand locus of f with zero equals the support of f.

Русский

Правый локус функции f по нулю совпадает с опорой функции f.

LaTeX

$$$ f.neLocus 0 = \operatorname{supp}(f) $$$

Lean4

@[simp]
theorem neLocus_zero_left : (0 : Π₀ a, N a).neLocus f = f.support :=
  (neLocus_comm _ _).trans (neLocus_zero_right _)

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

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

Разделы

Аффилиация

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