# mathlib3documentation

data.dfinsupp.ne_locus

# Locus of unequal values of finitely supported dependent functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.ne_locus 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.ne_locus f g coincides with dfinsupp.support (f - g).
def dfinsupp.ne_locus {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :

Given two finitely supported functions f g : α →₀ N, finsupp.ne_locus f g is the finset where f and g differ. This generalizes (f - g).support to situations without subtraction.

Equations
@[simp]
theorem dfinsupp.mem_ne_locus {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} {a : α} :
a f.ne_locus g f a g a
theorem dfinsupp.not_mem_ne_locus {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} {a : α} :
a f.ne_locus g f a = g a
@[simp]
theorem dfinsupp.coe_ne_locus {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :
(f.ne_locus g) = {x : α | f x g x}
@[simp]
theorem dfinsupp.ne_locus_eq_empty {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} :
f.ne_locus g = f = g
@[simp]
theorem dfinsupp.nonempty_ne_locus_iff {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} :
theorem dfinsupp.ne_locus_comm {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :
@[simp]
theorem dfinsupp.ne_locus_zero_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f : Π₀ (a : α), N a) :
@[simp]
theorem dfinsupp.ne_locus_zero_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f : Π₀ (a : α), N a) :
theorem dfinsupp.subset_map_range_ne_locus {α : Type u_1} {N : α Type u_2} [decidable_eq α] {M : α Type u_3} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (M a)] (f g : Π₀ (a : α), N a) {F : Π (a : α), N a M a} (F0 : (a : α), F a 0 = 0) :
F0 f).ne_locus F0 g) f.ne_locus g
theorem dfinsupp.zip_with_ne_locus_eq_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] {M : α Type u_3} {P : α Type u_4} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), has_zero (P a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (P a)] {F : Π (a : α), M a N a P a} (F0 : (a : α), F a 0 0 = 0) (f : Π₀ (a : α), M a) (g₁ g₂ : Π₀ (a : α), N a) (hF : (a : α) (f : M a), function.injective (λ (g : N a), F a f g)) :
F0 f g₁).ne_locus F0 f g₂) = g₁.ne_locus g₂
theorem dfinsupp.zip_with_ne_locus_eq_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] {M : α Type u_3} {P : α Type u_4} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), has_zero (P a)] [Π (a : α), decidable_eq (M a)] [Π (a : α), decidable_eq (P a)] {F : Π (a : α), M a N a P a} (F0 : (a : α), F a 0 0 = 0) (f₁ f₂ : Π₀ (a : α), M a) (g : Π₀ (a : α), N a) (hF : (a : α) (g : N a), function.injective (λ (f : M a), F a f g)) :
F0 f₁ g).ne_locus F0 f₂ g) = f₁.ne_locus f₂
theorem dfinsupp.map_range_ne_locus_eq {α : Type u_1} {N : α Type u_2} [decidable_eq α] {M : α Type u_3} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (M a)] (f g : Π₀ (a : α), N a) {F : Π (a : α), N a M a} (F0 : (a : α), F a 0 = 0) (hF : (a : α), function.injective (F a)) :
F0 f).ne_locus F0 g) = f.ne_locus g
@[simp]
theorem dfinsupp.ne_locus_add_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), ] (f g h : Π₀ (a : α), N a) :
(f + g).ne_locus (f + h) = g.ne_locus h
@[simp]
theorem dfinsupp.ne_locus_add_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), ] (f g h : Π₀ (a : α), N a) :
(f + h).ne_locus (g + h) = f.ne_locus g
@[simp]
theorem dfinsupp.ne_locus_neg_neg {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(-f).ne_locus (-g) = f.ne_locus g
theorem dfinsupp.ne_locus_neg {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(-f).ne_locus g = f.ne_locus (-g)
theorem dfinsupp.ne_locus_eq_support_sub {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus g = (f - g).support
@[simp]
theorem dfinsupp.ne_locus_sub_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g₁ g₂ : Π₀ (a : α), N a) :
(f - g₁).ne_locus (f - g₂) = g₁.ne_locus g₂
@[simp]
theorem dfinsupp.ne_locus_sub_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f₁ f₂ g : Π₀ (a : α), N a) :
(f₁ - g).ne_locus (f₂ - g) = f₁.ne_locus f₂
@[simp]
theorem dfinsupp.ne_locus_self_add_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus (f + g) = g.support
@[simp]
theorem dfinsupp.ne_locus_self_add_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(f + g).ne_locus f = g.support
@[simp]
theorem dfinsupp.ne_locus_self_sub_right {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus (f - g) = g.support
@[simp]
theorem dfinsupp.ne_locus_self_sub_left {α : Type u_1} {N : α Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(f - g).ne_locus f = g.support