mem_neLocus

Mathlib.Data.Finsupp.NeLocus

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

← MathLib Explorer

English

An element a belongs to f.neLocus g iff f(a) ≠ g(a).

Русский

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

LaTeX

$$$$ a \in f.neLocus g \iff f(a) \neq g(a). $$$$

Lean4

@[simp]
theorem mem_neLocus {f g : α →₀ N} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a := by
  simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff, and_iff_right_iff_imp] using Ne.ne_or_ne _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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