Locus of unequal values of finitely supported functions #

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

Main definition #

Finsupp.neLocus f g : Finset α, the finite subset of α where f and g differ.

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

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

Finset α

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

Equations

Finsupp.neLocus f g = Finset.filter (fun x => ↑f x ≠ ↑g x) (f.support ∪ g.support)

source

ink

@[simp]

theorem Finsupp.mem_neLocus {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] {f : α →₀ N} {g : α →₀ N} {a : α} :

a ∈ Finsupp.neLocus f g ↔ ↑f a ≠ ↑g a

source

ink

theorem Finsupp.not_mem_neLocus {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] {f : α →₀ N} {g : α →₀ N} {a : α} :

¬a ∈ Finsupp.neLocus f g ↔ ↑f a = ↑g a

source

ink

@[simp]

theorem Finsupp.coe_neLocus {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] (f : α →₀ N) (g : α →₀ N) :

↑(Finsupp.neLocus f g) = { x | ↑f x ≠ ↑g x }

source

ink

@[simp]

theorem Finsupp.neLocus_eq_empty {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] {f : α →₀ N} {g : α →₀ N} :

Finsupp.neLocus f g = ∅ ↔ f = g

source

ink

@[simp]

theorem Finsupp.nonempty_neLocus_iff {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] {f : α →₀ N} {g : α →₀ N} :

Finset.Nonempty (Finsupp.neLocus f g) ↔ f ≠ g

source

ink

theorem Finsupp.neLocus_comm {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus f g = Finsupp.neLocus g f

source

ink

@[simp]

theorem Finsupp.neLocus_zero_right {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] (f : α →₀ N) :

Finsupp.neLocus f 0 = f.support

source

ink

@[simp]

theorem Finsupp.neLocus_zero_left {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] (f : α →₀ N) :

Finsupp.neLocus 0 f = f.support

source

ink

theorem Finsupp.subset_mapRange_neLocus {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero N] [inst : DecidableEq M] [inst : Zero M] (f : α →₀ N) (g : α →₀ N) {F : N → M} (F0 : F 0 = 0) :

Finsupp.neLocus (Finsupp.mapRange F F0 f) (Finsupp.mapRange F F0 g) ⊆ Finsupp.neLocus f g

source

ink

theorem Finsupp.zipWith_neLocus_eq_left {α : Type u_4} {M : Type u_2} {N : Type u_1} {P : Type u_3} [inst : DecidableEq α] [inst : DecidableEq N] [inst : Zero M] [inst : DecidableEq P] [inst : Zero P] [inst : Zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f : α →₀ M) (g₁ : α →₀ N) (g₂ : α →₀ N) (hF : ∀ (f : M), Function.Injective fun g => F f g) :

Finsupp.neLocus (Finsupp.zipWith F F0 f g₁) (Finsupp.zipWith F F0 f g₂) = Finsupp.neLocus g₁ g₂

source

ink

theorem Finsupp.zipWith_neLocus_eq_right {α : Type u_4} {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : DecidableEq α] [inst : DecidableEq M] [inst : Zero M] [inst : DecidableEq P] [inst : Zero P] [inst : Zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f₁ : α →₀ M) (f₂ : α →₀ M) (g : α →₀ N) (hF : ∀ (g : N), Function.Injective fun f => F f g) :

Finsupp.neLocus (Finsupp.zipWith F F0 f₁ g) (Finsupp.zipWith F F0 f₂ g) = Finsupp.neLocus f₁ f₂

source

ink

theorem Finsupp.mapRange_neLocus_eq {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : DecidableEq α] [inst : DecidableEq N] [inst : DecidableEq M] [inst : Zero M] [inst : Zero N] (f : α →₀ N) (g : α →₀ N) {F : N → M} (F0 : F 0 = 0) (hF : Function.Injective F) :

Finsupp.neLocus (Finsupp.mapRange F F0 f) (Finsupp.mapRange F F0 g) = Finsupp.neLocus f g

source

ink

@[simp]

theorem Finsupp.neLocus_add_left {α : Type u_2} {N : Type u_1} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddLeftCancelMonoid N] (f : α →₀ N) (g : α →₀ N) (h : α →₀ N) :

Finsupp.neLocus (f + g) (f + h) = Finsupp.neLocus g h

source

ink

@[simp]

theorem Finsupp.neLocus_add_right {α : Type u_2} {N : Type u_1} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddRightCancelMonoid N] (f : α →₀ N) (g : α →₀ N) (h : α →₀ N) :

Finsupp.neLocus (f + h) (g + h) = Finsupp.neLocus f g

source

ink

@[simp]

theorem Finsupp.neLocus_neg_neg {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus (-f) (-g) = Finsupp.neLocus f g

source

ink

theorem Finsupp.neLocus_neg {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus (-f) g = Finsupp.neLocus f (-g)

source

ink

theorem Finsupp.neLocus_eq_support_sub {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus f g = (f - g).support

source

ink

@[simp]

theorem Finsupp.neLocus_sub_left {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g₁ : α →₀ N) (g₂ : α →₀ N) :

Finsupp.neLocus (f - g₁) (f - g₂) = Finsupp.neLocus g₁ g₂

source

ink

@[simp]

theorem Finsupp.neLocus_sub_right {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f₁ : α →₀ N) (f₂ : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus (f₁ - g) (f₂ - g) = Finsupp.neLocus f₁ f₂

source

ink

@[simp]

theorem Finsupp.neLocus_self_add_right {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus f (f + g) = g.support

source

ink

@[simp]

theorem Finsupp.neLocus_self_add_left {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus (f + g) f = g.support

source

ink

@[simp]

theorem Finsupp.neLocus_self_sub_right {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus f (f - g) = g.support

source

ink

@[simp]

theorem Finsupp.neLocus_self_sub_left {α : Type u_1} {N : Type u_2} [inst : DecidableEq α] [inst : DecidableEq N] [inst : AddGroup N] (f : α →₀ N) (g : α →₀ N) :

Finsupp.neLocus (f - g) f = g.support