Documentation

Mathlib.Data.Finsupp.NeLocus

Locus of unequal values of finitely supported functions #

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.neLocus f g coincides with Finsupp.support (f - g).

source
def Finsupp.neLocus {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] (f g : α →₀ N) :
Finset α

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
Instances For
    source
    @[simp]
    theorem Finsupp.mem_neLocus {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] {f g : α →₀ N} {a : α} :
    a ∈ f.neLocus g ↔ f a ≠ g a
    source
    theorem Finsupp.notMem_neLocus {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] {f g : α →₀ N} {a : α} :
    a ∉ f.neLocus g ↔ f a = g a
    source
    @[simp]
    theorem Finsupp.coe_neLocus {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] (f g : α →₀ N) :
    ↑(f.neLocus g) = {x : α | f x ≠ g x}
    source
    @[simp]
    theorem Finsupp.neLocus_eq_empty {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] {f g : α →₀ N} :
    f.neLocus g = ∅ ↔ f = g
    source
    @[simp]
    theorem Finsupp.nonempty_neLocus_iff {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] {f g : α →₀ N} :
    (f.neLocus g).Nonempty ↔ f ≠ g
    source
    theorem Finsupp.neLocus_comm {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] (f g : α →₀ N) :
    f.neLocus g = g.neLocus f
    source
    @[simp]
    theorem Finsupp.neLocus_zero_right {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] (f : α →₀ N) :
    f.neLocus 0 = f.support
    source
    @[simp]
    theorem Finsupp.neLocus_zero_left {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] (f : α →₀ N) :
    neLocus 0 f = f.support
    source
    theorem Finsupp.subset_mapRange_neLocus {α : Type u_1} {M : Type u_2} {N : Type u_3} [DecidableEq α] [DecidableEq N] [Zero N] [DecidableEq M] [Zero M] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0) :
    (mapRange F F0 f).neLocus (mapRange F F0 g) ⊆ f.neLocus g
    source
    theorem Finsupp.zipWith_neLocus_eq_left {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [DecidableEq α] [DecidableEq N] [Zero M] [DecidableEq P] [Zero P] [Zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f : α →₀ M) (g₁ g₂ : α →₀ N) (hF : ∀ (f : M), Function.Injective fun (g : N) => F f g) :
    (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂
    source
    theorem Finsupp.zipWith_neLocus_eq_right {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [DecidableEq α] [DecidableEq M] [Zero M] [DecidableEq P] [Zero P] [Zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f₁ f₂ : α →₀ M) (g : α →₀ N) (hF : ∀ (g : N), Function.Injective fun (f : M) => F f g) :
    (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂
    source
    theorem Finsupp.mapRange_neLocus_eq {α : Type u_1} {M : Type u_2} {N : Type u_3} [DecidableEq α] [DecidableEq N] [DecidableEq M] [Zero M] [Zero N] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0) (hF : Function.Injective F) :
    (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g
    source
    @[simp]
    theorem Finsupp.neLocus_add_left {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddLeftCancelMonoid N] (f g h : α →₀ N) :
    (f + g).neLocus (f + h) = g.neLocus h
    source
    @[simp]
    theorem Finsupp.neLocus_add_right {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddRightCancelMonoid N] (f g h : α →₀ N) :
    (f + h).neLocus (g + h) = f.neLocus g
    source
    @[simp]
    theorem Finsupp.neLocus_neg_neg {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    (-f).neLocus (-g) = f.neLocus g
    source
    theorem Finsupp.neLocus_neg {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    (-f).neLocus g = f.neLocus (-g)
    source
    theorem Finsupp.neLocus_eq_support_sub {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    f.neLocus g = (f - g).support
    source
    @[simp]
    theorem Finsupp.neLocus_sub_left {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g₁ g₂ : α →₀ N) :
    (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
    source
    @[simp]
    theorem Finsupp.neLocus_sub_right {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f₁ f₂ g : α →₀ N) :
    (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
    source
    @[simp]
    theorem Finsupp.neLocus_self_add_right {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    f.neLocus (f + g) = g.support
    source
    @[simp]
    theorem Finsupp.neLocus_self_add_left {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    (f + g).neLocus f = g.support
    source
    @[simp]
    theorem Finsupp.neLocus_self_sub_right {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    f.neLocus (f - g) = g.support
    source
    @[simp]
    theorem Finsupp.neLocus_self_sub_left {α : Type u_1} {N : Type u_3} [DecidableEq α] [DecidableEq N] [AddGroup N] (f g : α →₀ N) :
    (f - g).neLocus f = g.support