# 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 #

source
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 }

Instances For

source
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 }

Instances For

source
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)
source
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)
source
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
source
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
source
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
source
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
source
@[simp]
theorem Finset.coe_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) :
↑(s • t) = ↑s • ↑t
source
@[simp]
theorem Finset.coe_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) (t : Finset β) :
↑(s +ᵥ t) = ↑s +ᵥ ↑t
source
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
source
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
source
theorem Finset.card_smul_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
(s • t).card ≤ s.card * t.card
source
theorem Finset.card_vadd_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
(s +ᵥ t).card ≤ s.card * t.card
source
@[simp]
theorem Finset.empty_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (t : Finset β) :
∅ • t = ∅
source
@[simp]
theorem Finset.empty_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (t : Finset β) :
∅ +ᵥ t = ∅
source
@[simp]
theorem Finset.smul_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) :
s • ∅ = ∅
source
@[simp]
theorem Finset.vadd_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) :
s +ᵥ ∅ = ∅
source
@[simp]
theorem Finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
s • t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[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
source
@[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
source
theorem Finset.Nonempty.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
s.Nonempty → t.Nonempty → (s • t).Nonempty
source
theorem Finset.Nonempty.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty
source
theorem Finset.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
(s • t).Nonempty → s.Nonempty
source
theorem Finset.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
(s +ᵥ t).Nonempty → s.Nonempty
source
theorem Finset.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
(s • t).Nonempty → t.Nonempty
source
theorem Finset.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
(s +ᵥ t).Nonempty → t.Nonempty
source
theorem Finset.smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} (b : β) :
s • {b} = image (fun (x : α) => x • b) s
source
theorem Finset.vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} (b : β) :
s +ᵥ {b} = image (fun (x : α) => x +ᵥ b) s
source
theorem Finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (b : β) :
{a} • {b} = {a • b}
source
theorem Finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (b : β) :
{a} +ᵥ {b} = {a +ᵥ b}
source
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₂
source
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₂
source
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₂
source
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₂
source
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
source
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
source
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
source
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
source
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
source
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)
source
theorem Finset.smul_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ t₂ : Finset β} :
s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
source
theorem Finset.vadd_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ t₂ : Finset β} :
s +ᵥ t₁ ∪ t₂ = (s +ᵥ t₁) ∪ (s +ᵥ t₂)
source
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
source
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)
source
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₂
source
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₂)
source
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₂
source
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₂)
source
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₂
source
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₂)
source
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'`.

source
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 #

source
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 }

Instances For

source
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 }

Instances For

source
theorem Finset.smul_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
a • s = image (fun (x : β) => a • x) s
source
theorem Finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
a +ᵥ s = image (fun (x : β) => a +ᵥ x) s
source
theorem Finset.image_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
image (fun (x : β) => a • x) s = a • s
source
theorem Finset.image_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
image (fun (x : β) => a +ᵥ x) s = a +ᵥ s
source
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
source
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
source
@[simp]
theorem Finset.coe_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Finset β) :
↑(a • s) = a • ↑s
source
@[simp]
theorem Finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Finset β) :
↑(a +ᵥ s) = a +ᵥ ↑s
source
theorem Finset.smul_mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {b : β} :
b ∈ s → a • b ∈ a • s
source
theorem Finset.vadd_mem_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} {b : β} :
b ∈ s → a +ᵥ b ∈ a +ᵥ s
source
theorem Finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
(a • s).card ≤ s.card
source
theorem Finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
(a +ᵥ s).card ≤ s.card
source
@[simp]
theorem Finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) :
a • ∅ = ∅
source
@[simp]
theorem Finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) :
a +ᵥ ∅ = ∅
source
@[simp]
theorem Finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
a • s = ∅ ↔ s = ∅
source
@[simp]
theorem Finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
a +ᵥ s = ∅ ↔ s = ∅
source
@[simp]
theorem Finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
(a • s).Nonempty ↔ s.Nonempty
source
@[simp]
theorem Finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
(a +ᵥ s).Nonempty ↔ s.Nonempty
source
theorem Finset.Nonempty.smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} (hs : s.Nonempty) :
(a • s).Nonempty
source
theorem Finset.Nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} (hs : s.Nonempty) :
(a +ᵥ s).Nonempty
source
@[simp]
theorem Finset.singleton_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} (a : α) :
{a} • t = a • t
source
@[simp]
theorem Finset.singleton_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {t : Finset β} (a : α) :
{a} +ᵥ t = a +ᵥ t
source
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
source
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
source
@[simp]
theorem Finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {a : α} (b : β) :
a • {b} = {a • b}
source
@[simp]
theorem Finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {a : α} (b : β) :
a +ᵥ {b} = {a +ᵥ b}
source
theorem Finset.smul_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ s₂ : Finset β} {a : α} :
a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂
source
theorem Finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ s₂ : Finset β} {a : α} :
a +ᵥ s₁ ∪ s₂ = (a +ᵥ s₁) ∪ (a +ᵥ s₂)
source
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)
source
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)
source
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₂
source
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₂)
source
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
source
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
source
@[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
source
@[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 #

source
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 }

Instances For

source
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
source
@[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
source
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
source
@[simp]
theorem Finset.coe_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s t : Finset β) :
↑(s -ᵥ t) = ↑s -ᵥ ↑t
source
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
source
theorem Finset.vsub_card_le {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
(s -ᵥ t).card ≤ s.card * t.card
source
@[simp]
theorem Finset.empty_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (t : Finset β) :
∅ -ᵥ t = ∅
source
@[simp]
theorem Finset.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s : Finset β) :
s -ᵥ ∅ = ∅
source
@[simp]
theorem Finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
(s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
theorem Finset.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty
source
theorem Finset.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
(s -ᵥ t).Nonempty → s.Nonempty
source
theorem Finset.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t : Finset β} :
(s -ᵥ t).Nonempty → t.Nonempty
source
@[simp]
theorem Finset.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} (b : β) :
s -ᵥ {b} = image (fun (x : β) => x -ᵥ b) s
source
theorem Finset.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {t : Finset β} (a : β) :
{a} -ᵥ t = image (fun (x : β) => a -ᵥ x) t
source
theorem Finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (a b : β) :
{a} -ᵥ {b} = {a -ᵥ b}
source
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₂
source
theorem Finset.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t₁ t₂ : Finset β} :
t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
source
theorem Finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t : Finset β} :
s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
source
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
source
theorem Finset.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ s₂ t : Finset β} [DecidableEq β] :
s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
source
theorem Finset.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s t₁ t₂ : Finset β} [DecidableEq β] :
s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
source
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)
source
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₂)
source
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'`.

source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
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