Locus of unequal values of finitely supported dependent functions #

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

source

ink

def Dfinsupp.neLocus {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

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

source

ink

@[simp]

theorem Dfinsupp.mem_neLocus {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} {a : α} :

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

source

ink

theorem Dfinsupp.not_mem_neLocus {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} {a : α} :

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

source

ink

@[simp]

theorem Dfinsupp.coe_neLocus {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_eq_empty {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} :

Dfinsupp.neLocus f g = ∅ ↔ f = g

source

ink

@[simp]

theorem Dfinsupp.nonempty_neLocus_iff {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] {f : Dfinsupp fun a => N a} {g : Dfinsupp fun a => N a} :

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

source

ink

theorem Dfinsupp.neLocus_comm {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

Dfinsupp.neLocus f g = Dfinsupp.neLocus g f

source

ink

@[simp]

theorem Dfinsupp.neLocus_zero_right {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) :

Dfinsupp.neLocus f 0 = Dfinsupp.support f

source

ink

@[simp]

theorem Dfinsupp.neLocus_zero_left {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → Zero (N a)] (f : Dfinsupp fun a => N a) :

Dfinsupp.neLocus 0 f = Dfinsupp.support f

source

ink

theorem Dfinsupp.subset_mapRange_neLocus {α : Type u_3} {N : α → Type u_1} [inst : DecidableEq α] {M : α → Type u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → DecidableEq (M a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) {F : (a : α) → N a → M a} (F0 : ∀ (a : α), F a 0 = 0) :

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

source

ink

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

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

source

ink

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

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

source

ink

theorem Dfinsupp.mapRange_neLocus_eq {α : Type u_3} {N : α → Type u_1} [inst : DecidableEq α] {M : α → Type u_2} [inst : (a : α) → Zero (N a)] [inst : (a : α) → Zero (M a)] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → DecidableEq (M a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) {F : (a : α) → N a → M a} (F0 : ∀ (a : α), F a 0 = 0) (hF : ∀ (a : α), Function.Injective (F a)) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_add_left {α : Type u_2} {N : α → Type u_1} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddLeftCancelMonoid (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) (h : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_add_right {α : Type u_2} {N : α → Type u_1} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddRightCancelMonoid (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) (h : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_neg_neg {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

theorem Dfinsupp.neLocus_neg {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

theorem Dfinsupp.neLocus_eq_support_sub {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_sub_left {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g₁ : Dfinsupp fun a => N a) (g₂ : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_sub_right {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f₁ : Dfinsupp fun a => N a) (f₂ : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_self_add_right {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_self_add_left {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_self_sub_right {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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

source

ink

@[simp]

theorem Dfinsupp.neLocus_self_sub_left {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (N a)] [inst : (a : α) → AddGroup (N a)] (f : Dfinsupp fun a => N a) (g : Dfinsupp fun a => N a) :

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