nonempty_neLocus_iff

Mathlib.Data.DFinsupp.NeLocus

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

English

The difference locus of f and g is nonempty if and only if f and g are not equal.

Русский

Локус различий между f и g непуст, если и только если f ≠ g.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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