mathlib3 documentation

data.finsupp.ne_locus

Locus of unequal values of finitely supported functions #

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

Let α N be two Types, assume that N has a 0 and let f g : α →₀ N be finitely supported functions.

Main definition #

In the case in which N is an additive group, finsupp.ne_locus f g coincides with finsupp.support (f - g).

def finsupp.ne_locus {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f g : α →₀ N) :

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