English
neLocus(f,g) is the Finset of indices where f and g differ, i.e., (f.support ∪ g.support).filter (λ x, f x ≠ g x).
Русский
neLocus(f,g) — это конечное множество индексов, на которых функции f и g различны; определяется как (f.support ∪ g.support).filter (λ x, f x ≠ g x).
LaTeX
$$$$ \\operatorname{neLocus}(f,g) = (f\\text{.support} \\cup g\\text{.support}).\\text{filter}\\bigl(\\lambda x. f\,x \\neq g\,x\\bigr) $$$$
Lean4
/-- Given two finitely supported functions `f g : α →₀ N`, `Finsupp.neLocus f g` is the `Finset`
where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction. -/
def neLocus (f g : Π₀ a, N a) : Finset α :=
(f.support ∪ g.support).filter fun x ↦ f x ≠ g x
