coe_neLocus

Mathlib.Data.Finsupp.NeLocus

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

English

The coercion of f.neLocus g equals the set {x | f(x) ≠ g(x)}.

Русский

Приведение к множеству f.neLocus g даёт множество {x | f(x) ≠ g(x)}.

LaTeX

$$$$ \uparrow\,(f.neLocus g) = \{x \mid f(x) \neq g(x)\}. $$$$

Lean4

@[simp]
theorem coe_neLocus : ↑(f.neLocus g) = {x | f x ≠ g x} := by
  ext
  exact mem_neLocus

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

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

Разделы

Аффилиация

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