mathlib3 documentation

data.dfinsupp.ne_locus

Locus of unequal values of finitely supported dependent functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
def dfinsupp.ne_locus {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :
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.

Equations
source
@[simp]
theorem dfinsupp.mem_ne_locus {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} {a : α} :
a ∈ f.ne_locus g ↔ ⇑f a ≠ ⇑g a
source
theorem dfinsupp.not_mem_ne_locus {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} {a : α} :
a ∉ f.ne_locus g ↔ ⇑f a = ⇑g a
source
@[simp]
theorem dfinsupp.coe_ne_locus {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :
↑(f.ne_locus g) = {x : α | ⇑f x ≠ ⇑g x}
source
@[simp]
theorem dfinsupp.ne_locus_eq_empty {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} :
f.ne_locus g = ∅ ↔ f = g
source
@[simp]
theorem dfinsupp.nonempty_ne_locus_iff {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] {f g : Π₀ (a : α), N a} :
(f.ne_locus g).nonempty ↔ f ≠ g
source
theorem dfinsupp.ne_locus_comm {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus g = g.ne_locus f
source
@[simp]
theorem dfinsupp.ne_locus_zero_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f : Π₀ (a : α), N a) :
f.ne_locus 0 = f.support
source
@[simp]
theorem dfinsupp.ne_locus_zero_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), has_zero (N a)] (f : Π₀ (a : α), N a) :
0.ne_locus f = f.support
source
theorem dfinsupp.subset_map_range_ne_locus {α : Type u_1} {N : α → Type u_2} [decidable_eq α] {M : α → Type u_3} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (M a)] (f g : Π₀ (a : α), N a) {F : Π (a : α), N a → M a} (F0 : ∀ (a : α), F a 0 = 0) :
(dfinsupp.map_range F F0 f).ne_locus (dfinsupp.map_range F F0 g) ⊆ f.ne_locus g
source
theorem dfinsupp.zip_with_ne_locus_eq_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] {M : α → Type u_3} {P : α → Type u_4} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), has_zero (P a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (P a)] {F : Π (a : α), M a → N a → P a} (F0 : ∀ (a : α), F a 0 0 = 0) (f : Π₀ (a : α), M a) (g₁ g₂ : Π₀ (a : α), N a) (hF : ∀ (a : α) (f : M a), function.injective (λ (g : N a), F a f g)) :
(dfinsupp.zip_with F F0 f g₁).ne_locus (dfinsupp.zip_with F F0 f g₂) = g₁.ne_locus g₂
source
theorem dfinsupp.zip_with_ne_locus_eq_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] {M : α → Type u_3} {P : α → Type u_4} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), has_zero (P a)] [Π (a : α), decidable_eq (M a)] [Π (a : α), decidable_eq (P a)] {F : Π (a : α), M a → N a → P a} (F0 : ∀ (a : α), F a 0 0 = 0) (f₁ f₂ : Π₀ (a : α), M a) (g : Π₀ (a : α), N a) (hF : ∀ (a : α) (g : N a), function.injective (λ (f : M a), F a f g)) :
(dfinsupp.zip_with F F0 f₁ g).ne_locus (dfinsupp.zip_with F F0 f₂ g) = f₁.ne_locus f₂
source
theorem dfinsupp.map_range_ne_locus_eq {α : Type u_1} {N : α → Type u_2} [decidable_eq α] {M : α → Type u_3} [Π (a : α), has_zero (N a)] [Π (a : α), has_zero (M a)] [Π (a : α), decidable_eq (N a)] [Π (a : α), decidable_eq (M a)] (f g : Π₀ (a : α), N a) {F : Π (a : α), N a → M a} (F0 : ∀ (a : α), F a 0 = 0) (hF : ∀ (a : α), function.injective (F a)) :
(dfinsupp.map_range F F0 f).ne_locus (dfinsupp.map_range F F0 g) = f.ne_locus g
source
@[simp]
theorem dfinsupp.ne_locus_add_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_left_cancel_monoid (N a)] (f g h : Π₀ (a : α), N a) :
(f + g).ne_locus (f + h) = g.ne_locus h
source
@[simp]
theorem dfinsupp.ne_locus_add_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_right_cancel_monoid (N a)] (f g h : Π₀ (a : α), N a) :
(f + h).ne_locus (g + h) = f.ne_locus g
source
@[simp]
theorem dfinsupp.ne_locus_neg_neg {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(-f).ne_locus (-g) = f.ne_locus g
source
theorem dfinsupp.ne_locus_neg {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(-f).ne_locus g = f.ne_locus (-g)
source
theorem dfinsupp.ne_locus_eq_support_sub {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus g = (f - g).support
source
@[simp]
theorem dfinsupp.ne_locus_sub_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g₁ g₂ : Π₀ (a : α), N a) :
(f - g₁).ne_locus (f - g₂) = g₁.ne_locus g₂
source
@[simp]
theorem dfinsupp.ne_locus_sub_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f₁ f₂ g : Π₀ (a : α), N a) :
(f₁ - g).ne_locus (f₂ - g) = f₁.ne_locus f₂
source
@[simp]
theorem dfinsupp.ne_locus_self_add_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus (f + g) = g.support
source
@[simp]
theorem dfinsupp.ne_locus_self_add_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(f + g).ne_locus f = g.support
source
@[simp]
theorem dfinsupp.ne_locus_self_sub_right {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
f.ne_locus (f - g) = g.support
source
@[simp]
theorem dfinsupp.ne_locus_self_sub_left {α : Type u_1} {N : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (N a)] [Π (a : α), add_group (N a)] (f g : Π₀ (a : α), N a) :
(f - g).ne_locus f = g.support