coe_neLocus

Mathlib.Data.DFinsupp.NeLocus

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

English

The set of indices where f and g differ is exactly the set { x ∈ α | f(x) ≠ g(x) }, considered as a subset of α.

Русский

Множество индексов, на которых f и g различаются, есть { x ∈ α | f(x) ≠ g(x) }.

LaTeX

$$$ (f \neLocus g)^{\uparrow} = \{ x \in \alpha \mid f(x) \neq g(x) \} $$$

Lean4

@[simp]
theorem coe_neLocus : ↑(f.neLocus g) = {x | f x ≠ g x} :=
  Set.ext fun _x ↦ mem_neLocus

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

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

Разделы

Аффилиация

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