# Documentation

Mathlib.Data.Dfinsupp.NeLocus

# Locus of unequal values of finitely supported dependent functions #

Let N : α → Type* be a type family, assume that N a has a 0 for all a : α and let f g : Π₀ a, N a be finitely supported dependent functions.

## Main definition #

• Dfinsupp.neLocus f g : finset α, the finite subset of α where f and g differ. In the case in which N a is an additive group for all a, Dfinsupp.neLocus f g coincides with Dfinsupp.support (f - g).
def Dfinsupp.neLocus {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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.

Equations
@[simp]
theorem Dfinsupp.mem_neLocus {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} {a : α} :
a f a g a
theorem Dfinsupp.not_mem_neLocus {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} {a : α} :
¬a f a = g a
@[simp]
theorem Dfinsupp.coe_neLocus {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
↑() = { x | f x g x }
@[simp]
theorem Dfinsupp.neLocus_eq_empty {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} :
f = g
@[simp]
theorem Dfinsupp.nonempty_neLocus_iff {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} :
f g
theorem Dfinsupp.neLocus_comm {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_zero_right {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_zero_left {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) :
theorem Dfinsupp.subset_mapRange_neLocus {α : Type u_3} {N : αType u_1} [inst : ] {M : αType u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → DecidableEq (M a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) {F : (a : α) → N aM a} (F0 : ∀ (a : α), F a 0 = 0) :
theorem Dfinsupp.zipWith_neLocus_eq_left {α : Type u_4} {N : αType u_1} [inst : ] {M : αType u_3} {P : αType u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → Zero (P a)] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → DecidableEq (P a)] {F : (a : α) → M aN aP a} (F0 : ∀ (a : α), F a 0 0 = 0) (f : Dfinsupp fun a => M a) (g₁ : Dfinsupp fun a => N a) (g₂ : Dfinsupp fun a => N a) (hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g) :
theorem Dfinsupp.zipWith_neLocus_eq_right {α : Type u_4} {N : αType u_3} [inst : ] {M : αType u_1} {P : αType u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → Zero (P a)] [inst : (a : α) → DecidableEq (M a)] [inst : (a : α) → DecidableEq (P a)] {F : (a : α) → M aN aP a} (F0 : ∀ (a : α), F a 0 0 = 0) (f₁ : Dfinsupp fun a => M a) (f₂ : Dfinsupp fun a => M a) (g : Dfinsupp fun a => N a) (hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g) :
theorem Dfinsupp.mapRange_neLocus_eq {α : Type u_3} {N : αType u_1} [inst : ] {M : αType u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → DecidableEq (M a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) {F : (a : α) → N aM a} (F0 : ∀ (a : α), F a 0 = 0) (hF : ∀ (a : α), Function.Injective (F a)) :
@[simp]
theorem Dfinsupp.neLocus_add_left {α : Type u_2} {N : αType u_1} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddLeftCancelMonoid (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) (h : Dfinsupp fun a => N a) :
Dfinsupp.neLocus (f + g) (f + h) =
@[simp]
theorem Dfinsupp.neLocus_add_right {α : Type u_2} {N : αType u_1} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddRightCancelMonoid (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) (h : Dfinsupp fun a => N a) :
Dfinsupp.neLocus (f + h) (g + h) =
@[simp]
theorem Dfinsupp.neLocus_neg_neg {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
theorem Dfinsupp.neLocus_neg {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
=
theorem Dfinsupp.neLocus_eq_support_sub {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_sub_left {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g₁ : Dfinsupp fun a => N a) (g₂ : Dfinsupp fun a => N a) :
Dfinsupp.neLocus (f - g₁) (f - g₂) = Dfinsupp.neLocus g₁ g₂
@[simp]
theorem Dfinsupp.neLocus_sub_right {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f₁ : Dfinsupp fun a => N a) (f₂ : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
Dfinsupp.neLocus (f₁ - g) (f₂ - g) = Dfinsupp.neLocus f₁ f₂
@[simp]
theorem Dfinsupp.neLocus_self_add_right {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_self_add_left {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_self_sub_right {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :
@[simp]
theorem Dfinsupp.neLocus_self_sub_left {α : Type u_1} {N : αType u_2} [inst : ] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :