Pointwise operations of finsets

This file defines pointwise algebraic operations on finsets.

Main declarations

For finsets s and t:

• s +ᵥ t (Finset.vadd): Scalar addition, finset of all x +ᵥ y where x ∈ s and y ∈ t.
• s • t (Finset.smul): Scalar multiplication, finset of all x • y where x ∈ s and y ∈ t.
• s -ᵥ t (Finset.vsub): Scalar subtraction, finset of all x -ᵥ y where x ∈ s and y ∈ t.
• a • s (Finset.smulFinset): Scaling, finset of all a • x where x ∈ s.
• a +ᵥ s (Finset.vaddFinset): Translation, finset of all a +ᵥ x where x ∈ s.

For α a semigroup/monoid, Finset α is a semigroup/monoid. As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].

Implementation notes

We put all instances in the scope Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the scope to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp).

Tags

finset multiplication, finset addition, pointwise addition, pointwise multiplication, pointwise subtraction

Scalar addition/multiplication of finsets

def Finset.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] : SMul (Finset α) (Finset β)

The pointwise product of two finsets s and t: s • t = {x • y | x ∈ s, y ∈ t}.

Equations

• Finset.smul = { smul := Finset.image₂ fun (x1 : α) (x2 : β) => x1 • x2 }

def Finset.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] : VAdd (Finset α) (Finset β)

The pointwise sum of two finsets s and t: s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}.

Equations

• Finset.vadd = { vadd := Finset.image₂ fun (x1 : α) (x2 : β) => x1 +ᵥ x2 }

theorem Finset.smul_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : s • t = image (fun (p : α × β) => p.1 • p.2) (s ×ˢ t)

theorem Finset.vadd_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : s +ᵥ t = image (fun (p : α × β) => p.1 +ᵥ p.2) (s ×ˢ t)

theorem Finset.image_smul_product {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : image (fun (x : α × β) => x.1 • x.2) (s ×ˢ t) = s • t

theorem Finset.image_vadd_product {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : image (fun (x : α × β) => x.1 +ᵥ x.2) (s ×ˢ t) = s +ᵥ t

theorem Finset.mem_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {x : β} : x ∈ s • t ↔ ∃ y ∈ s, ∃ z ∈ t, y • z = x

theorem Finset.mem_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} {x : β} : x ∈ s +ᵥ t ↔ ∃ y ∈ s, ∃ z ∈ t, y +ᵥ z = x

@[simp]

theorem Finset.coe_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) : ↑(s • t) = ↑s • ↑t

@[simp]

theorem Finset.coe_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) (t : Finset β) : ↑(s +ᵥ t) = ↑s +ᵥ ↑t

theorem Finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {a : α} {b : β} : a ∈ s → b ∈ t → a • b ∈ s • t

theorem Finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} {a : α} {b : β} : a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t

theorem Finset.card_smul_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : (s • t).card ≤ s.card * t.card

theorem Finset.card_vadd_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : (s +ᵥ t).card ≤ s.card * t.card

@[simp]

theorem Finset.empty_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (t : Finset β) : ∅ • t = ∅

@[simp]

theorem Finset.empty_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (t : Finset β) : ∅ +ᵥ t = ∅

@[simp]

theorem Finset.smul_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) : s • ∅ = ∅

@[simp]

theorem Finset.vadd_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) : s +ᵥ ∅ = ∅

@[simp]

theorem Finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : s • t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Finset.vadd_nonempty_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Finset.Nonempty.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : s.Nonempty → t.Nonempty → (s • t).Nonempty

theorem Finset.Nonempty.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty

theorem Finset.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : (s • t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : (s +ᵥ t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : (s • t).Nonempty → t.Nonempty

theorem Finset.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : (s +ᵥ t).Nonempty → t.Nonempty

theorem Finset.smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} (b : β) : s • {b} = image (fun (x : α) => x • b) s

theorem Finset.vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} (b : β) : s +ᵥ {b} = image (fun (x : α) => x +ᵥ b) s

theorem Finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (b : β) : {a} • {b} = {a • b}

theorem Finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (b : β) : {a} +ᵥ {b} = {a +ᵥ b}

theorem Finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂

theorem Finset.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂

theorem Finset.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ t₂ : Finset β} : t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂

theorem Finset.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ t₂ : Finset β} : t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂

theorem Finset.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t : Finset β} : s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t

theorem Finset.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t : Finset β} : s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t

theorem Finset.smul_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t u : Finset β} : s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u

theorem Finset.vadd_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t u : Finset β} : s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u

theorem Finset.union_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t : Finset β} [DecidableEq α] : (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

theorem Finset.union_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t : Finset β} [DecidableEq α] : (s₁ ∪ s₂) +ᵥ t = (s₁ +ᵥ t) ∪ (s₂ +ᵥ t)

theorem Finset.smul_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ t₂ : Finset β} : s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂

theorem Finset.vadd_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ t₂ : Finset β} : s +ᵥ t₁ ∪ t₂ = (s +ᵥ t₁) ∪ (s +ᵥ t₂)

theorem Finset.inter_smul_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t : Finset β} [DecidableEq α] : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t

theorem Finset.inter_vadd_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t : Finset β} [DecidableEq α] : s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)

theorem Finset.smul_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ t₂ : Finset β} : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂

theorem Finset.vadd_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ t₂ : Finset β} : s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)

theorem Finset.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} [DecidableEq α] : (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Finset.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} [DecidableEq α] : s₁ ∩ s₂ +ᵥ t₁ ∪ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)

theorem Finset.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} [DecidableEq α] : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Finset.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} [DecidableEq α] : (s₁ ∪ s₂) +ᵥ t₁ ∩ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)

theorem Finset.subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {u : Finset β} {s : Set α} {t : Set β} : ↑u ⊆ s • t → ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t'

If a finset u is contained in the scalar product of two sets s • t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' • t'.

theorem Finset.subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {u : Finset β} {s : Set α} {t : Set β} : ↑u ⊆ s +ᵥ t → ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' +ᵥ t'

If a finset u is contained in the scalar sum of two sets s +ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' +ᵥ t'.

Translation/scaling of finsets

def Finset.smulFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] : SMul α (Finset β)

The scaling of a finset s by a scalar a: a • s = {a • x | x ∈ s}.

Equations

• Finset.smulFinset = { smul := fun (a : α) => Finset.image fun (x : β) => a • x }

def Finset.vaddFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] : VAdd α (Finset β)

The translation of a finset s by a vector a: a +ᵥ s = {a +ᵥ x | x ∈ s}.

Equations

• Finset.vaddFinset = { vadd := fun (a : α) => Finset.image fun (x : β) => a +ᵥ x }

theorem Finset.smul_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : a • s = image (fun (x : β) => a • x) s

theorem Finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : a +ᵥ s = image (fun (x : β) => a +ᵥ x) s

theorem Finset.image_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : image (fun (x : β) => a • x) s = a • s

theorem Finset.image_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : image (fun (x : β) => a +ᵥ x) s = a +ᵥ s

theorem Finset.mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {x : β} : x ∈ a • s ↔ ∃ y ∈ s, a • y = x

theorem Finset.mem_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} {x : β} : x ∈ a +ᵥ s ↔ ∃ y ∈ s, a +ᵥ y = x

@[simp]

theorem Finset.coe_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Finset β) : ↑(a • s) = a • ↑s

@[simp]

theorem Finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Finset β) : ↑(a +ᵥ s) = a +ᵥ ↑s

theorem Finset.smul_mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {b : β} : b ∈ s → a • b ∈ a • s

theorem Finset.vadd_mem_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} {b : β} : b ∈ s → a +ᵥ b ∈ a +ᵥ s

theorem Finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : (a • s).card ≤ s.card

theorem Finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : (a +ᵥ s).card ≤ s.card

@[simp]

theorem Finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) : a • ∅ = ∅

@[simp]

theorem Finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) : a +ᵥ ∅ = ∅

@[simp]

theorem Finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : a • s = ∅ ↔ s = ∅

@[simp]

theorem Finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : a +ᵥ s = ∅ ↔ s = ∅

@[simp]

theorem Finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : (a • s).Nonempty ↔ s.Nonempty

@[simp]

theorem Finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : (a +ᵥ s).Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} (hs : s.Nonempty) : (a • s).Nonempty

theorem Finset.Nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} (hs : s.Nonempty) : (a +ᵥ s).Nonempty

@[simp]

theorem Finset.singleton_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} (a : α) : {a} • t = a • t

@[simp]

theorem Finset.singleton_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {t : Finset β} (a : α) : {a} +ᵥ t = a +ᵥ t

theorem Finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s t : Finset β} {a : α} : s ⊆ t → a • s ⊆ a • t

theorem Finset.vadd_finset_subset_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s t : Finset β} {a : α} : s ⊆ t → a +ᵥ s ⊆ a +ᵥ t

@[simp]

theorem Finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {a : α} (b : β) : a • {b} = {a • b}

@[simp]

theorem Finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {a : α} (b : β) : a +ᵥ {b} = {a +ᵥ b}

theorem Finset.smul_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset β} {a : α} : a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂

theorem Finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset β} {a : α} : a +ᵥ s₁ ∪ s₂ = (a +ᵥ s₁) ∪ (a +ᵥ s₂)

theorem Finset.smul_finset_insert {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (b : β) (s : Finset β) : a • insert b s = insert (a • b) (a • s)

theorem Finset.vadd_finset_insert {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (b : β) (s : Finset β) : a +ᵥ insert b s = insert (a +ᵥ b) (a +ᵥ s)

theorem Finset.smul_finset_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset β} {a : α} : a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ a • s₂

theorem Finset.vadd_finset_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset β} {a : α} : a +ᵥ s₁ ∩ s₂ ⊆ (a +ᵥ s₁) ∩ (a +ᵥ s₂)

theorem Finset.smul_finset_subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} {a : α} {s : Finset α} : a ∈ s → a • t ⊆ s • t

theorem Finset.vadd_finset_subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {t : Finset β} {a : α} {s : Finset α} : a ∈ s → a +ᵥ t ⊆ s +ᵥ t

@[simp]

theorem Finset.biUnion_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) : (s.biUnion fun (x : α) => x • t) = s • t

@[simp]

theorem Finset.biUnion_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) (t : Finset β) : (s.biUnion fun (x : α) => x +ᵥ t) = s +ᵥ t

Instances

Scalar subtraction of finsets

def Finset.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] : VSub (Finset α) (Finset β)

The pointwise subtraction of two finsets s and t: s -ᵥ t = {x -ᵥ y | x ∈ s, y ∈ t}.

Equations

• Finset.vsub = { vsub := Finset.image₂ fun (x1 x2 : β) => x1 -ᵥ x2 }

theorem Finset.vsub_def {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : s -ᵥ t = image₂ (fun (x1 x2 : β) => x1 -ᵥ x2) s t

@[simp]

theorem Finset.image_vsub_product {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : image₂ (fun (x1 x2 : β) => x1 -ᵥ x2) s t = s -ᵥ t

theorem Finset.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} {a : α} : a ∈ s -ᵥ t ↔ ∃ b ∈ s, ∃ c ∈ t, b -ᵥ c = a

@[simp]

theorem Finset.coe_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s t : Finset β) : ↑(s -ᵥ t) = ↑s -ᵥ ↑t

theorem Finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} {b c : β} : b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t

theorem Finset.vsub_card_le {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : (s -ᵥ t).card ≤ s.card * t.card

@[simp]

theorem Finset.empty_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (t : Finset β) : ∅ -ᵥ t = ∅

@[simp]

theorem Finset.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s : Finset β) : s -ᵥ ∅ = ∅

@[simp]

theorem Finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : (s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Finset.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty

theorem Finset.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : (s -ᵥ t).Nonempty → s.Nonempty

theorem Finset.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} : (s -ᵥ t).Nonempty → t.Nonempty

@[simp]

theorem Finset.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} (b : β) : s -ᵥ {b} = image (fun (x : β) => x -ᵥ b) s

theorem Finset.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {t : Finset β} (a : β) : {a} -ᵥ t = image (fun (x : β) => a -ᵥ x) t

theorem Finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (a b : β) : {a} -ᵥ {b} = {a -ᵥ b}

theorem Finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t₁ t₂ : Finset β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂

theorem Finset.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t₁ t₂ : Finset β} : t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂

theorem Finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t : Finset β} : s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t

theorem Finset.vsub_subset_iff {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} {u : Finset α} : s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u

theorem Finset.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t : Finset β} [DecidableEq β] : s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)

theorem Finset.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t₁ t₂ : Finset β} [DecidableEq β] : s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)

theorem Finset.inter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t : Finset β} [DecidableEq β] : s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)

theorem Finset.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t₁ t₂ : Finset β} [DecidableEq β] : s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)

theorem Finset.subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {u : Finset α} {s t : Set β} : ↑u ⊆ s -ᵥ t → ∃ (s' : Finset β) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t'

If a finset u is contained in the pointwise subtraction of two sets s -ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' -ᵥ t'.

theorem Finset.op_smul_finset_smul_eq_smul_smul_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ] (a : α) (s : Finset β) (t : Finset γ) (h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c) : (MulOpposite.op a • s) • t = s • a • t

theorem Finset.op_vadd_finset_vadd_eq_vadd_vadd_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [VAdd αᵃᵒᵖ β] [VAdd β γ] [VAdd α γ] (a : α) (s : Finset β) (t : Finset γ) (h : ∀ (a : α) (b : β) (c : γ), (AddOpposite.op a +ᵥ b) +ᵥ c = b +ᵥ a +ᵥ c) : (AddOpposite.op a +ᵥ s) +ᵥ t = s +ᵥ a +ᵥ t

theorem Finset.image_smul_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Finset β) : (∀ (b : β), f (a • b) = a • f b) → image f (a • s) = a • image f s

theorem Finset.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [VAdd α β] [VAdd α γ] (f : β → γ) (a : α) (s : Finset β) : (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → image f (a +ᵥ s) = a +ᵥ image f s

@[simp]

theorem Set.toFinset_smul {α : Type u_2} {β : Type u_3} [SMul α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s • t)] : (s • t).toFinset = s.toFinset • t.toFinset

@[simp]

theorem Set.toFinset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s +ᵥ t)] : (s +ᵥ t).toFinset = s.toFinset +ᵥ t.toFinset

theorem Set.Finite.toFinset_smul {α : Type u_2} {β : Type u_3} [SMul α β] [DecidableEq β] {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) (hf : (s • t).Finite := ⋯) : hf.toFinset = hs.toFinset • ht.toFinset

theorem Set.Finite.toFinset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] [DecidableEq β] {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) (hf : (s +ᵥ t).Finite := ⋯) : hf.toFinset = hs.toFinset +ᵥ ht.toFinset

@[simp]

theorem Set.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a • s)] : (a • s).toFinset = a • s.toFinset

@[simp]

theorem Set.toFinset_vadd_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a +ᵥ s)] : (a +ᵥ s).toFinset = a +ᵥ s.toFinset

theorem Set.Finite.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {a : α} {s : Set β} (hs : s.Finite) (hf : (a • s).Finite := ⋯) : hf.toFinset = a • hs.toFinset

theorem Set.Finite.toFinset_vadd_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {a : α} {s : Set β} (hs : s.Finite) (hf : (a +ᵥ s).Finite := ⋯) : hf.toFinset = a +ᵥ hs.toFinset

@[simp]

theorem Set.toFinset_vsub {α : Type u_2} {β : Type u_3} [DecidableEq α] [VSub α β] (s t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s -ᵥ t)] : (s -ᵥ t).toFinset = s.toFinset -ᵥ t.toFinset

theorem Set.Finite.toFinset_vsub {α : Type u_2} {β : Type u_3} [DecidableEq α] [VSub α β] {s t : Set β} (hs : s.Finite) (ht : t.Finite) (hf : (s -ᵥ t).Finite := ⋯) : hf.toFinset = hs.toFinset -ᵥ ht.toFinset