notMem_neLocus

Mathlib.Data.Finsupp.NeLocus

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

English

An element a does not belong to f.neLocus g iff f(a) = g(a).

Русский

Элемент a не принадлежит f.neLocus g тогда, когда f(a) = g(a).

LaTeX

$$$$ a \notin f.neLocus g \iff f(a) = g(a). $$$$

Lean4

theorem notMem_neLocus {f g : α →₀ N} {a : α} : a ∉ f.neLocus g ↔ f a = g a :=
  mem_neLocus.not.trans not_ne_iff

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

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

Разделы

Аффилиация

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