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 #
finsupp.ne_locus f g : finset α, the finite subset ofαwherefandgdiffer.
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) :
finset α
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.
@[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 : α} :
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 : α} :
@[simp]
theorem
finsupp.coe_ne_locus
{α : Type u_1}
{N : Type u_3}
[decidable_eq α]
[decidable_eq N]
[has_zero N]
(f g : α →₀ N) :
@[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} :
@[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) :
(finsupp.map_range F F0 f).ne_locus (finsupp.map_range F F0 g) ⊆ f.ne_locus g
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) :
(finsupp.map_range F F0 f).ne_locus (finsupp.map_range F F0 g) = f.ne_locus g
@[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) :
@[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) :
@[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) :
theorem
finsupp.ne_locus_neg
{α : Type u_1}
{N : Type u_3}
[decidable_eq α]
[decidable_eq N]
[add_group N]
(f g : α →₀ N) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :