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.sdiv): Scalar division, 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

@[instance_reducible]

def Finset.smul {α : Type u_1} {β : Type u_2} [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 }

@[instance_reducible]

def Finset.vadd {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : s • t = image (fun (p : α × β) => p.1 • p.2) (s ×ˢ t)

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.inter_smul_union_subset_union {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} [DecidableEq α] : (s₁ ∪ s₂) +ᵥ t₁ ∩ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)

theorem Finset.subset_smul {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [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

@[instance_reducible]

def Finset.smulFinset {α : Type u_1} {β : Type u_2} [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 }

@[instance_reducible]

def Finset.vaddFinset {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : a • s = image (fun (x : β) => a • x) s

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[deprecated Finset.card_smul_finset_le (since := "2026-04-16")]

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

Alias of Finset.card_smul_finset_le.

@[deprecated Finset.card_vadd_finset_le (since := "2026-04-16")]

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

Alias of Finset.card_vadd_finset_le.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

Instances

Scalar division and subtraction of finsets

@[instance_reducible]

def Finset.sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] : SDiv (Finset α) (Finset β)

The pointwise division of two finsets s and t: s /ₛ t = {x /ₛ y | x ∈ s, y ∈ t}.

Equations

• Finset.sdiv = { sdiv := Finset.image₂ fun (x1 x2 : β) => x1 /ₛ x2 }

@[instance_reducible]

def Finset.vsub {α : Type u_1} {β : Type u_2} [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.sdiv_def {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : s /ₛ t = image₂ (fun (x1 x2 : β) => x1 /ₛ x2) s t

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

@[simp]

theorem Finset.image_sdiv_product {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : image₂ (fun (x1 x2 : β) => x1 /ₛ x2) s t = s /ₛ t

@[simp]

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

theorem Finset.mem_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} {a : α} : a ∈ s /ₛ t ↔ ∃ b ∈ s, ∃ c ∈ t, b /ₛ c = a

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

@[simp]

theorem Finset.coe_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] (s t : Finset β) : ↑(s /ₛ t) = ↑s /ₛ ↑t

@[simp]

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

theorem Finset.sdiv_mem_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} {b c : β} : b ∈ s → c ∈ t → b /ₛ c ∈ s /ₛ t

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

theorem Finset.sdiv_card_le {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : (s /ₛ t).card ≤ s.card * t.card

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

@[simp]

theorem Finset.empty_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] (t : Finset β) : ∅ /ₛ t = ∅

@[simp]

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

@[simp]

theorem Finset.sdiv_empty {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] (s : Finset β) : s /ₛ ∅ = ∅

@[simp]

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

@[simp]

theorem Finset.sdiv_eq_empty {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : s /ₛ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

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

@[simp]

theorem Finset.sdiv_nonempty {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : (s /ₛ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

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

theorem Finset.Nonempty.sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : s.Nonempty → t.Nonempty → (s /ₛ t).Nonempty

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

theorem Finset.Nonempty.of_sdiv_left {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : (s /ₛ t).Nonempty → s.Nonempty

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

theorem Finset.Nonempty.of_sdiv_right {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} : (s /ₛ t).Nonempty → t.Nonempty

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

@[simp]

theorem Finset.sdiv_singleton {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s : Finset β} (b : β) : s /ₛ {b} = image (fun (x : β) => x /ₛ b) s

@[simp]

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

theorem Finset.singleton_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {t : Finset β} (a : β) : {a} /ₛ t = image (fun (x : β) => a /ₛ x) t

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

theorem Finset.singleton_sdiv_singleton {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] (a b : β) : {a} /ₛ {b} = {a /ₛ b}

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

theorem Finset.sdiv_subset_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s₁ s₂ t₁ t₂ : Finset β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ /ₛ t₁ ⊆ s₂ /ₛ t₂

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

theorem Finset.sdiv_subset_sdiv_left {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t₁ t₂ : Finset β} : t₁ ⊆ t₂ → s /ₛ t₁ ⊆ s /ₛ t₂

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

theorem Finset.sdiv_subset_sdiv_right {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s₁ s₂ t : Finset β} : s₁ ⊆ s₂ → s₁ /ₛ t ⊆ s₂ /ₛ t

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

theorem Finset.sdiv_subset_iff {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t : Finset β} {u : Finset α} : s /ₛ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x /ₛ y ∈ u

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

theorem Finset.union_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s₁ s₂ t : Finset β} [DecidableEq β] : s₁ ∪ s₂ /ₛ t = s₁ /ₛ t ∪ (s₂ /ₛ t)

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

theorem Finset.sdiv_union {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t₁ t₂ : Finset β} [DecidableEq β] : s /ₛ (t₁ ∪ t₂) = s /ₛ t₁ ∪ (s /ₛ t₂)

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

theorem Finset.inter_sdiv_subset {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s₁ s₂ t : Finset β} [DecidableEq β] : s₁ ∩ s₂ /ₛ t ⊆ (s₁ /ₛ t) ∩ (s₂ /ₛ t)

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

theorem Finset.sdiv_inter_subset {α : Type u_1} {β : Type u_2} [SDiv α β] [DecidableEq α] {s t₁ t₂ : Finset β} [DecidableEq β] : s /ₛ t₁ ∩ t₂ ⊆ (s /ₛ t₁) ∩ (s /ₛ t₂)

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

theorem Finset.subset_sdiv {α : Type u_1} {β : Type u_2} [SDiv α β] [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 division 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_vsub {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [DecidableEq β] [SMul α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a • s)] : (a • s).toFinset = a • s.toFinset

@[simp]

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

theorem Set.Finite.toFinset_smul_set {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [DecidableEq β] [VAdd α β] {a : α} {s : Set β} (hs : s.Finite) (hf : (a +ᵥ s).Finite := ⋯) : hf.toFinset = a +ᵥ hs.toFinset

@[simp]

theorem Set.toFinset_sdiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [SDiv α β] (s t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s /ₛ t)] : (s /ₛ t).toFinset = s.toFinset /ₛ t.toFinset

@[simp]

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

theorem Set.Finite.toFinset_sdiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [SDiv α β] {s t : Set β} (hs : s.Finite) (ht : t.Finite) (hf : (s /ₛ t).Finite := ⋯) : hf.toFinset = hs.toFinset /ₛ ht.toFinset

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