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).

def DFinsupp.neLocus {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (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)

@[simp]

theorem DFinsupp.mem_neLocus {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] {f : Π₀ (a : α), N a} {g : Π₀ (a : α), N a} {a : α} : a ∈ DFinsupp.neLocus f g ↔ f a ≠ g a

theorem DFinsupp.not_mem_neLocus {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] {f : Π₀ (a : α), N a} {g : Π₀ (a : α), N a} {a : α} : a ∉ DFinsupp.neLocus f g ↔ f a = g a

@[simp]

theorem DFinsupp.coe_neLocus {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : ↑(DFinsupp.neLocus f g) = {x : α | f x ≠ g x}

@[simp]

theorem DFinsupp.neLocus_eq_empty {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] {f : Π₀ (a : α), N a} {g : Π₀ (a : α), N a} : DFinsupp.neLocus f g = ∅ ↔ f = g

@[simp]

theorem DFinsupp.nonempty_neLocus_iff {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] {f : Π₀ (a : α), N a} {g : Π₀ (a : α), N a} : (DFinsupp.neLocus f g).Nonempty ↔ f ≠ g

theorem DFinsupp.neLocus_comm {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus f g = DFinsupp.neLocus g f

@[simp]

theorem DFinsupp.neLocus_zero_right {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] (f : Π₀ (a : α), N a) : DFinsupp.neLocus f 0 = DFinsupp.support f

@[simp]

theorem DFinsupp.neLocus_zero_left {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → Zero (N a)] (f : Π₀ (a : α), N a) : DFinsupp.neLocus 0 f = DFinsupp.support f

theorem DFinsupp.subset_mapRange_neLocus {α : Type u_1} {N : α → Type u_2} [DecidableEq α] {M : α → Type u_3} [(a : α) → Zero (N a)] [(a : α) → Zero (M a)] [(a : α) → DecidableEq (N a)] [(a : α) → DecidableEq (M a)] (f : Π₀ (a : α), N a) (g : Π₀ (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

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

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

theorem DFinsupp.mapRange_neLocus_eq {α : Type u_1} {N : α → Type u_2} [DecidableEq α] {M : α → Type u_3} [(a : α) → Zero (N a)] [(a : α) → Zero (M a)] [(a : α) → DecidableEq (N a)] [(a : α) → DecidableEq (M a)] (f : Π₀ (a : α), N a) (g : Π₀ (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

@[simp]

theorem DFinsupp.neLocus_add_left {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddLeftCancelMonoid (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) (h : Π₀ (a : α), N a) : DFinsupp.neLocus (f + g) (f + h) = DFinsupp.neLocus g h

@[simp]

theorem DFinsupp.neLocus_add_right {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddRightCancelMonoid (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) (h : Π₀ (a : α), N a) : DFinsupp.neLocus (f + h) (g + h) = DFinsupp.neLocus f g

@[simp]

theorem DFinsupp.neLocus_neg_neg {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus (-f) (-g) = DFinsupp.neLocus f g

theorem DFinsupp.neLocus_neg {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus (-f) g = DFinsupp.neLocus f (-g)

theorem DFinsupp.neLocus_eq_support_sub {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus f g = DFinsupp.support (f - g)

@[simp]

theorem DFinsupp.neLocus_sub_left {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g₁ : Π₀ (a : α), N a) (g₂ : Π₀ (a : α), N a) : DFinsupp.neLocus (f - g₁) (f - g₂) = DFinsupp.neLocus g₁ g₂

@[simp]

theorem DFinsupp.neLocus_sub_right {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f₁ : Π₀ (a : α), N a) (f₂ : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus (f₁ - g) (f₂ - g) = DFinsupp.neLocus f₁ f₂

@[simp]

theorem DFinsupp.neLocus_self_add_right {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus f (f + g) = DFinsupp.support g

@[simp]

theorem DFinsupp.neLocus_self_add_left {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus (f + g) f = DFinsupp.support g

@[simp]

theorem DFinsupp.neLocus_self_sub_right {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus f (f - g) = DFinsupp.support g

@[simp]

theorem DFinsupp.neLocus_self_sub_left {α : Type u_1} {N : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (N a)] [(a : α) → AddGroup (N a)] (f : Π₀ (a : α), N a) (g : Π₀ (a : α), N a) : DFinsupp.neLocus (f - g) f = DFinsupp.support g