nonempty_neLocus_iff

Mathlib.Data.Finsupp.NeLocus

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

English

f.neLocus g is nonempty iff f ≠ g.

Русский

f.neLocus g непусто тогда, когда f ≠ g.

LaTeX

$$$$ (f.neLocus g).Nonempty \iff f \neq g. $$$$

Lean4

@[simp]
theorem nonempty_neLocus_iff {f g : α →₀ N} : (f.neLocus g).Nonempty ↔ f ≠ g :=
  Finset.nonempty_iff_ne_empty.trans neLocus_eq_empty.not

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

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

Разделы

Аффилиация

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