Pointwise operations of finsets

This file defines pointwise algebraic operations on finsets.

Main declarations

For finsets s and t:

• 0 (Finset.zero): The singleton {0}.
• 1 (Finset.one): The singleton {1}.
• -s (Finset.neg): Negation, finset of all -x where x ∈ s.
• s⁻¹ (Finset.inv): Inversion, finset of all x⁻¹ where x ∈ s.
• s + t (Finset.add): Addition, finset of all x + y where x ∈ s and y ∈ t.
• s * t (Finset.mul): Multiplication, finset of all x * y where x ∈ s and y ∈ t.
• s - t (Finset.sub): Subtraction, finset of all x - y where x ∈ s and y ∈ t.
• s / t (Finset.div): Division, finset of all x / y where x ∈ s and y ∈ 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 locale 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 locale 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

0/1 as finsets

def Finset.zero {α : Type u_2} [Zero α] : Zero (Finset α)

The finset 0 : Finset α is defined as {0} in locale Pointwise.

def Finset.one {α : Type u_2} [One α] : One (Finset α)

The finset 1 : Finset α is defined as {1} in locale Pointwise.

@[simp]

theorem Finset.mem_zero {α : Type u_2} [Zero α] {a : α} : a ∈ 0 ↔ a = 0

@[simp]

theorem Finset.mem_one {α : Type u_2} [One α] {a : α} : a ∈ 1 ↔ a = 1

@[simp]

theorem Finset.coe_zero {α : Type u_2} [Zero α] : ↑0 = 0

@[simp]

theorem Finset.coe_one {α : Type u_2} [One α] : ↑1 = 1

@[simp]

theorem Finset.zero_subset {α : Type u_2} [Zero α] {s : Finset α} : 0 ⊆ s ↔ 0 ∈ s

@[simp]

theorem Finset.one_subset {α : Type u_2} [One α] {s : Finset α} : 1 ⊆ s ↔ 1 ∈ s

theorem Finset.singleton_zero {α : Type u_2} [Zero α] : {0} = 0

theorem Finset.singleton_one {α : Type u_2} [One α] : {1} = 1

theorem Finset.zero_mem_zero {α : Type u_2} [Zero α] : 0 ∈ 0

theorem Finset.one_mem_one {α : Type u_2} [One α] : 1 ∈ 1

theorem Finset.zero_nonempty {α : Type u_2} [Zero α] : Finset.Nonempty 0

theorem Finset.one_nonempty {α : Type u_2} [One α] : Finset.Nonempty 1

@[simp]

theorem Finset.map_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α ↪ β} : Finset.map f 0 = {↑f 0}

@[simp]

theorem Finset.map_one {α : Type u_2} {β : Type u_3} [One α] {f : α ↪ β} : Finset.map f 1 = {↑f 1}

@[simp]

theorem Finset.image_zero {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] {f : α → β} : Finset.image f 0 = {f 0}

@[simp]

theorem Finset.image_one {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] {f : α → β} : Finset.image f 1 = {f 1}

theorem Finset.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Finset α} : s ⊆ 0 ↔ s = ∅ ∨ s = 0

theorem Finset.subset_one_iff_eq {α : Type u_2} [One α] {s : Finset α} : s ⊆ 1 ↔ s = ∅ ∨ s = 1

theorem Finset.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Finset α} (h : Finset.Nonempty s) : s ⊆ 0 ↔ s = 0

theorem Finset.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Finset α} (h : Finset.Nonempty s) : s ⊆ 1 ↔ s = 1

@[simp]

theorem Finset.card_zero {α : Type u_2} [Zero α] : Finset.card 0 = 1

@[simp]

theorem Finset.card_one {α : Type u_2} [One α] : Finset.card 1 = 1

def Finset.singletonZeroHom {α : Type u_2} [Zero α] : ZeroHom α (Finset α)

The singleton operation as a ZeroHom.

def Finset.singletonOneHom {α : Type u_2} [One α] : OneHom α (Finset α)

The singleton operation as a OneHom.

@[simp]

theorem Finset.coe_singletonZeroHom {α : Type u_2} [Zero α] : ↑Finset.singletonZeroHom = singleton

@[simp]

theorem Finset.coe_singletonOneHom {α : Type u_2} [One α] : ↑Finset.singletonOneHom = singleton

@[simp]

theorem Finset.singletonZeroHom_apply {α : Type u_2} [Zero α] (a : α) : ↑Finset.singletonZeroHom a = {a}

@[simp]

theorem Finset.singletonOneHom_apply {α : Type u_2} [One α] (a : α) : ↑Finset.singletonOneHom a = {a}

theorem Finset.imageZeroHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) : Finset.image (↑f) 0 = 0

def Finset.imageZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) : ZeroHom (Finset α) (Finset β)

Lift a ZeroHom to Finset via image

@[simp]

theorem Finset.imageZeroHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageZeroHom f) s = Finset.image (↑f) s

@[simp]

theorem Finset.imageOneHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [OneHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageOneHom f) s = Finset.image (↑f) s

def Finset.imageOneHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [OneHomClass F α β] (f : F) : OneHom (Finset α) (Finset β)

Lift a OneHom to Finset via image.

Finset negation/inversion

def Finset.neg {α : Type u_2} [DecidableEq α] [Neg α] : Neg (Finset α)

The pointwise negation of finset -s is defined as {-x | x ∈ s} in locale Pointwise.

def Finset.inv {α : Type u_2} [DecidableEq α] [Inv α] : Inv (Finset α)

The pointwise inversion of finset s⁻¹ is defined as {x⁻¹ | x ∈ s} in locale Pointwise.

theorem Finset.neg_def {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : -s = Finset.image (fun x => -x) s

theorem Finset.inv_def {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹ = Finset.image (fun x => x⁻¹) s

theorem Finset.image_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.image (fun x => -x) s = -s

theorem Finset.image_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.image (fun x => x⁻¹) s = s⁻¹

theorem Finset.mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {x : α} : x ∈ -s ↔ ∃ y, y ∈ s ∧ -y = x

theorem Finset.mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {x : α} : x ∈ s⁻¹ ↔ ∃ y, y ∈ s ∧ y⁻¹ = x

theorem Finset.neg_mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {a : α} (ha : a ∈ s) : -a ∈ -s

theorem Finset.inv_mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {a : α} (ha : a ∈ s) : a⁻¹ ∈ s⁻¹

theorem Finset.card_neg_le {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.card (-s) ≤ Finset.card s

theorem Finset.card_inv_le {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.card s⁻¹ ≤ Finset.card s

@[simp]

theorem Finset.neg_empty {α : Type u_2} [DecidableEq α] [Neg α] : -∅ = ∅

@[simp]

theorem Finset.inv_empty {α : Type u_2} [DecidableEq α] [Inv α] : ∅⁻¹ = ∅

@[simp]

theorem Finset.neg_nonempty_iff {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty (-s) ↔ Finset.Nonempty s

@[simp]

theorem Finset.inv_nonempty_iff {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.Nonempty s⁻¹ ↔ Finset.Nonempty s

theorem Finset.Nonempty.inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.Nonempty s → Finset.Nonempty s⁻¹

Alias of the reverse direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.Nonempty s⁻¹ → Finset.Nonempty s

Alias of the forward direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty (-s) → Finset.Nonempty s

theorem Finset.Nonempty.neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty s → Finset.Nonempty (-s)

theorem Finset.neg_subset_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {t : Finset α} (h : s ⊆ t) : -s ⊆ -t

theorem Finset.inv_subset_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {t : Finset α} (h : s ⊆ t) : s⁻¹ ⊆ t⁻¹

@[simp]

theorem Finset.neg_singleton {α : Type u_2} [DecidableEq α] [Neg α] (a : α) : -{a} = {-a}

@[simp]

theorem Finset.inv_singleton {α : Type u_2} [DecidableEq α] [Inv α] (a : α) : {a}⁻¹ = {a⁻¹}

@[simp]

theorem Finset.neg_insert {α : Type u_2} [DecidableEq α] [Neg α] (a : α) (s : Finset α) : -insert a s = insert (-a) (-s)

@[simp]

theorem Finset.inv_insert {α : Type u_2} [DecidableEq α] [Inv α] (a : α) (s : Finset α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

@[simp]

theorem Finset.coe_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : ↑(-s) = -↑s

@[simp]

theorem Finset.coe_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : ↑s⁻¹ = (↑s)⁻¹

@[simp]

theorem Finset.card_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : Finset.card (-s) = Finset.card s

@[simp]

theorem Finset.card_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : Finset.card s⁻¹ = Finset.card s

@[simp]

theorem Finset.preimage_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : Finset.preimage s Neg.neg (_ : Set.InjOn Neg.neg (Neg.neg ⁻¹' ↑s)) = -s

@[simp]

theorem Finset.preimage_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : Finset.preimage s Inv.inv (_ : Set.InjOn Inv.inv (Inv.inv ⁻¹' ↑s)) = s⁻¹

Finset addition/multiplication

def Finset.add {α : Type u_2} [DecidableEq α] [Add α] : Add (Finset α)

The pointwise addition of finsets s + t is defined as {x + y | x ∈ s, y ∈ t} in locale Pointwise.

def Finset.mul {α : Type u_2} [DecidableEq α] [Mul α] : Mul (Finset α)

The pointwise multiplication of finsets s * t and t is defined as {x * y | x ∈ s, y ∈ t} in locale Pointwise.

theorem Finset.add_def {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : s + t = Finset.image (fun p => p.fst + p.snd) (s ×ˢ t)

theorem Finset.mul_def {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : s * t = Finset.image (fun p => p.fst * p.snd) (s ×ˢ t)

theorem Finset.image_add_product {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.image (fun x => x.fst + x.snd) (s ×ˢ t) = s + t

theorem Finset.image_mul_product {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.image (fun x => x.fst * x.snd) (s ×ˢ t) = s * t

theorem Finset.mem_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {x : α} : x ∈ s + t ↔ ∃ y z, y ∈ s ∧ z ∈ t ∧ y + z = x

theorem Finset.mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {x : α} : x ∈ s * t ↔ ∃ y z, y ∈ s ∧ z ∈ t ∧ y * z = x

@[simp]

theorem Finset.coe_add {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

@[simp]

theorem Finset.coe_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : ↑(s * t) = ↑s * ↑t

theorem Finset.add_mem_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a + b ∈ s + t

theorem Finset.mul_mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a * b ∈ s * t

theorem Finset.card_add_le {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.card (s + t) ≤ Finset.card s * Finset.card t

theorem Finset.card_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.card (s * t) ≤ Finset.card s * Finset.card t

theorem Finset.card_add_iff {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.card (s + t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun p => p.fst + p.snd) (↑s ×ˢ ↑t)

theorem Finset.card_mul_iff {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.card (s * t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun p => p.fst * p.snd) (↑s ×ˢ ↑t)

@[simp]

theorem Finset.empty_add {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) : ∅ + s = ∅

@[simp]

theorem Finset.empty_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : ∅ * s = ∅

@[simp]

theorem Finset.add_empty {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) : s + ∅ = ∅

@[simp]

theorem Finset.mul_empty {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : s * ∅ = ∅

@[simp]

theorem Finset.add_eq_empty {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : s + t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.mul_eq_empty {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : s * t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.add_nonempty {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s + t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

@[simp]

theorem Finset.mul_nonempty {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s + t)

theorem Finset.Nonempty.mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s * t)

theorem Finset.Nonempty.of_add_left {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s + t) → Finset.Nonempty s

theorem Finset.Nonempty.of_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) → Finset.Nonempty s

theorem Finset.Nonempty.of_add_right {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s + t) → Finset.Nonempty t

theorem Finset.Nonempty.of_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) → Finset.Nonempty t

theorem Finset.add_singleton {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} (a : α) : s + {a} = Finset.image (fun x => x + a) s

theorem Finset.mul_singleton {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} (a : α) : s * {a} = Finset.image (fun x => x * a) s

theorem Finset.singleton_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} (a : α) : {a} + s = Finset.image ((fun x x_1 => x + x_1) a) s

theorem Finset.singleton_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} (a : α) : {a} * s = Finset.image ((fun x x_1 => x * x_1) a) s

@[simp]

theorem Finset.singleton_add_singleton {α : Type u_2} [DecidableEq α] [Add α] (a : α) (b : α) : {a} + {b} = {a + b}

@[simp]

theorem Finset.singleton_mul_singleton {α : Type u_2} [DecidableEq α] [Mul α] (a : α) (b : α) : {a} * {b} = {a * b}

theorem Finset.add_subset_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ + t₁ ⊆ s₂ + t₂

theorem Finset.mul_subset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂

theorem Finset.add_subset_add_left {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂

theorem Finset.mul_subset_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂

theorem Finset.add_subset_add_right {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t

theorem Finset.mul_subset_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t

theorem Finset.add_subset_iff {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {u : Finset α} : s + t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x + y ∈ u

theorem Finset.mul_subset_iff {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {u : Finset α} : s * t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x * y ∈ u

theorem Finset.union_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)

theorem Finset.union_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t

theorem Finset.add_union {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)

theorem Finset.mul_union {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂

theorem Finset.inter_add_subset {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)

theorem Finset.inter_mul_subset {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)

theorem Finset.add_inter_subset {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)

theorem Finset.mul_inter_subset {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)

theorem Finset.inter_add_union_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Finset.inter_mul_union_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Finset.union_add_inter_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Finset.union_mul_inter_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Finset.subset_add {α : Type u_2} [DecidableEq α] [Add α] {u : Finset α} {s : Set α} {t : Set α} : ↑u ⊆ s + t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' + t'

If a finset u is contained in the sum 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_mul {α : Type u_2} [DecidableEq α] [Mul α] {u : Finset α} {s : Set α} {t : Set α} : ↑u ⊆ s * t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'

If a finset u is contained in the 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.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) {s : Finset α} {t : Finset α} : Finset.image (↑f) (s + t) = Finset.image (↑f) s + Finset.image (↑f) t

theorem Finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) {s : Finset α} {t : Finset α} : Finset.image (↑f) (s * t) = Finset.image (↑f) s * Finset.image (↑f) t

def Finset.singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] : AddHom α (Finset α)

The singleton operation as an AddHom.

theorem Finset.singletonAddHom.proof_1 {α : Type u_1} [DecidableEq α] [Add α] : ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}

def Finset.singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] : α →ₙ* Finset α

The singleton operation as a MulHom.

@[simp]

theorem Finset.coe_singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] : ↑Finset.singletonAddHom = singleton

@[simp]

theorem Finset.coe_singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] : ↑Finset.singletonMulHom = singleton

@[simp]

theorem Finset.singletonAddHom_apply {α : Type u_2} [DecidableEq α] [Add α] (a : α) : ↑Finset.singletonAddHom a = {a}

@[simp]

theorem Finset.singletonMulHom_apply {α : Type u_2} [DecidableEq α] [Mul α] (a : α) : ↑Finset.singletonMulHom a = {a}

theorem Finset.imageAddHom.proof_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) : ∀ (x x_1 : Finset α), Finset.image (↑f) (x + x_1) = Finset.image (↑f) x + Finset.image (↑f) x_1

def Finset.imageAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) : AddHom (Finset α) (Finset β)

Lift an AddHom to Finset via image

@[simp]

theorem Finset.imageAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageAddHom f) s = Finset.image (↑f) s

@[simp]

theorem Finset.imageMulHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageMulHom f) s = Finset.image (↑f) s

def Finset.imageMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) : Finset α →ₙ* Finset β

Lift a MulHom to Finset via image.

Finset subtraction/division

def Finset.sub {α : Type u_2} [DecidableEq α] [Sub α] : Sub (Finset α)

The pointwise subtraction of finsets s - t is defined as {x - y | x ∈ s, y ∈ t} in locale Pointwise.

def Finset.div {α : Type u_2} [DecidableEq α] [Div α] : Div (Finset α)

The pointwise division of finsets s / t is defined as {x / y | x ∈ s, y ∈ t} in locale Pointwise.

theorem Finset.sub_def {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : s - t = Finset.image (fun p => p.fst - p.snd) (s ×ˢ t)

theorem Finset.div_def {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : s / t = Finset.image (fun p => p.fst / p.snd) (s ×ˢ t)

theorem Finset.add_image_prod {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.image (fun x => x.fst - x.snd) (s ×ˢ t) = s - t

theorem Finset.image_div_prod {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.image (fun x => x.fst / x.snd) (s ×ˢ t) = s / t

theorem Finset.mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {a : α} : a ∈ s - t ↔ ∃ b c, b ∈ s ∧ c ∈ t ∧ b - c = a

theorem Finset.mem_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {a : α} : a ∈ s / t ↔ ∃ b c, b ∈ s ∧ c ∈ t ∧ b / c = a

@[simp]

theorem Finset.coe_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) (t : Finset α) : ↑(s - t) = ↑s - ↑t

@[simp]

theorem Finset.coe_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) (t : Finset α) : ↑(s / t) = ↑s / ↑t

theorem Finset.sub_mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a - b ∈ s - t

theorem Finset.div_mem_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a / b ∈ s / t

theorem Finset.sub_card_le {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.card (s - t) ≤ Finset.card s * Finset.card t

theorem Finset.div_card_le {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.card (s / t) ≤ Finset.card s * Finset.card t

@[simp]

theorem Finset.empty_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : ∅ - s = ∅

@[simp]

theorem Finset.empty_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : ∅ / s = ∅

@[simp]

theorem Finset.sub_empty {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : s - ∅ = ∅

@[simp]

theorem Finset.div_empty {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : s / ∅ = ∅

@[simp]

theorem Finset.sub_eq_empty {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : s - t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.div_eq_empty {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : s / t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.sub_nonempty {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s - t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

@[simp]

theorem Finset.div_nonempty {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s - t)

theorem Finset.Nonempty.div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s / t)

theorem Finset.Nonempty.of_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s - t) → Finset.Nonempty s

theorem Finset.Nonempty.of_div_left {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) → Finset.Nonempty s

theorem Finset.Nonempty.of_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s - t) → Finset.Nonempty t

theorem Finset.Nonempty.of_div_right {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) → Finset.Nonempty t

@[simp]

theorem Finset.sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) : s - {a} = Finset.image (fun x => x - a) s

@[simp]

theorem Finset.div_singleton {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) : s / {a} = Finset.image (fun x => x / a) s

@[simp]

theorem Finset.singleton_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) : {a} - s = Finset.image ((fun x x_1 => x - x_1) a) s

@[simp]

theorem Finset.singleton_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) : {a} / s = Finset.image ((fun x x_1 => x / x_1) a) s

theorem Finset.singleton_sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] (a : α) (b : α) : {a} - {b} = {a - b}

theorem Finset.singleton_div_singleton {α : Type u_2} [DecidableEq α] [Div α] (a : α) (b : α) : {a} / {b} = {a / b}

theorem Finset.sub_subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ - t₁ ⊆ s₂ - t₂

theorem Finset.div_subset_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂

theorem Finset.sub_subset_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂

theorem Finset.div_subset_div_left {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

theorem Finset.sub_subset_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t

theorem Finset.div_subset_div_right {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

theorem Finset.sub_subset_iff {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {u : Finset α} : s - t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x - y ∈ u

theorem Finset.div_subset_iff {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {u : Finset α} : s / t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x / y ∈ u

theorem Finset.union_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)

theorem Finset.union_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

theorem Finset.sub_union {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)

theorem Finset.div_union {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

theorem Finset.inter_sub_subset {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)

theorem Finset.inter_div_subset {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} : s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

theorem Finset.sub_inter_subset {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)

theorem Finset.div_inter_subset {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

theorem Finset.inter_sub_union_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Finset.inter_div_union_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Finset.union_sub_inter_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Finset.union_div_inter_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Finset.subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {u : Finset α} {s : Set α} {t : Set α} : ↑u ⊆ s - t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' - t'

If a finset u is contained in the sum 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_div {α : Type u_2} [DecidableEq α] [Div α] {u : Finset α} {s : Set α} {t : Set α} : ↑u ⊆ s / t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t'

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

Instances

def Finset.nsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] : SMul ℕ (Finset α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a Finset. See note [pointwise nat action].

def Finset.npow {α : Type u_2} [DecidableEq α] [One α] [Mul α] : Pow (Finset α) ℕ

Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a Finset. See note [pointwise nat action].

def Finset.zsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] [Neg α] : SMul ℤ (Finset α)

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a Finset. See note [pointwise nat action].

def Finset.zpow {α : Type u_2} [DecidableEq α] [One α] [Mul α] [Inv α] : Pow (Finset α) ℤ

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a Finset. See note [pointwise nat action].

theorem Finset.addSemigroup.proof_1 {α : Type u_1} [DecidableEq α] [AddSemigroup α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

def Finset.addSemigroup {α : Type u_2} [DecidableEq α] [AddSemigroup α] : AddSemigroup (Finset α)

Finset α is an AddSemigroup under pointwise operations if α is.

def Finset.semigroup {α : Type u_2} [DecidableEq α] [Semigroup α] : Semigroup (Finset α)

Finset α is a Semigroup under pointwise operations if α is.

theorem Finset.addCommSemigroup.proof_1 {α : Type u_1} [DecidableEq α] [AddCommSemigroup α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

def Finset.addCommSemigroup {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] : AddCommSemigroup (Finset α)

Finset α is an AddCommSemigroup under pointwise operations if α is.

def Finset.commSemigroup {α : Type u_2} [DecidableEq α] [CommSemigroup α] : CommSemigroup (Finset α)

Finset α is a CommSemigroup under pointwise operations if α is.

theorem Finset.inter_add_union_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s : Finset α} {t : Finset α} : s ∩ t + (s ∪ t) ⊆ s + t

theorem Finset.inter_mul_union_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s : Finset α} {t : Finset α} : s ∩ t * (s ∪ t) ⊆ s * t

theorem Finset.union_add_inter_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s : Finset α} {t : Finset α} : s ∪ t + s ∩ t ⊆ s + t

theorem Finset.union_mul_inter_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s : Finset α} {t : Finset α} : (s ∪ t) * (s ∩ t) ⊆ s * t

theorem Finset.addZeroClass.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.addZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] : ↑{0} = {0}

def Finset.addZeroClass {α : Type u_2} [DecidableEq α] [AddZeroClass α] : AddZeroClass (Finset α)

Finset α is an AddZeroClass under pointwise operations if α is.

def Finset.mulOneClass {α : Type u_2} [DecidableEq α] [MulOneClass α] : MulOneClass (Finset α)

Finset α is a MulOneClass under pointwise operations if α is.

theorem Finset.subset_add_left {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) {t : Finset α} (ht : 0 ∈ t) : s ⊆ s + t

theorem Finset.subset_mul_left {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) {t : Finset α} (ht : 1 ∈ t) : s ⊆ s * t

theorem Finset.subset_add_right {α : Type u_2} [DecidableEq α] [AddZeroClass α] {s : Finset α} (t : Finset α) (hs : 0 ∈ s) : t ⊆ s + t

theorem Finset.subset_mul_right {α : Type u_2} [DecidableEq α] [MulOneClass α] {s : Finset α} (t : Finset α) (hs : 1 ∈ s) : t ⊆ s * t

theorem Finset.singletonAddMonoidHom.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (x : α) (y : α) : AddHom.toFun Finset.singletonAddHom (x + y) = AddHom.toFun Finset.singletonAddHom x + AddHom.toFun Finset.singletonAddHom y

theorem Finset.singletonAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] : ZeroHom.toFun Finset.singletonZeroHom 0 = 0

def Finset.singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : α →+ Finset α

The singleton operation as an AddMonoidHom.

def Finset.singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : α →* Finset α

The singleton operation as a MonoidHom.

@[simp]

theorem Finset.coe_singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : ↑Finset.singletonAddMonoidHom = singleton

@[simp]

theorem Finset.coe_singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : ↑Finset.singletonMonoidHom = singleton

@[simp]

theorem Finset.singletonAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (a : α) : ↑Finset.singletonAddMonoidHom a = {a}

@[simp]

theorem Finset.singletonMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (a : α) : ↑Finset.singletonMonoidHom a = {a}

theorem Finset.coeAddMonoidHom.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.coeAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] : ↑0 = 0

noncomputable def Finset.coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : Finset α →+ Set α

The coercion from Finset to set as an AddMonoidHom.

noncomputable def Finset.coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : Finset α →* Set α

The coercion from Finset to Set as a MonoidHom.

@[simp]

theorem Finset.coe_coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : ↑Finset.coeAddMonoidHom = CoeTC.coe

@[simp]

theorem Finset.coe_coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : ↑Finset.coeMonoidHom = CoeTC.coe

@[simp]

theorem Finset.coeAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) : ↑Finset.coeAddMonoidHom s = ↑s

@[simp]

theorem Finset.coeMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) : ↑Finset.coeMonoidHom s = ↑s

theorem Finset.imageAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) : ZeroHom.toFun (Finset.imageZeroHom f) 0 = 0

def Finset.imageAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) : Finset α →+ Finset β

Lift an add_monoid_hom to Finset via image

theorem Finset.imageAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) (x : Finset α) (y : Finset α) : AddHom.toFun (Finset.imageAddHom f) (x + y) = AddHom.toFun (Finset.imageAddHom f) x + AddHom.toFun (Finset.imageAddHom f) y

@[simp]

theorem Finset.imageAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) : ∀ (a : Finset α), ↑(Finset.imageAddMonoidHom f) a = AddHom.toFun (Finset.imageAddHom f) a

@[simp]

theorem Finset.imageMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) : ∀ (a : Finset α), ↑(Finset.imageMonoidHom f) a = MulHom.toFun (Finset.imageMulHom f) a

def Finset.imageMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) : Finset α →* Finset β

Lift a MonoidHom to Finset via image.

@[simp]

theorem Finset.coe_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

@[simp]

theorem Finset.coe_pow {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ℕ) : ↑(s ^ n) = ↑s ^ n

def Finset.addMonoid {α : Type u_2} [DecidableEq α] [AddMonoid α] : AddMonoid (Finset α)

Finset α is an AddMonoid under pointwise operations if α is.

theorem Finset.addMonoid.proof_1 {α : Type u_1} [AddMonoid α] : ↑0 = 0

theorem Finset.addMonoid.proof_2 {α : Type u_1} [DecidableEq α] [AddMonoid α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.addMonoid.proof_3 {α : Type u_1} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

def Finset.monoid {α : Type u_2} [DecidableEq α] [Monoid α] : Monoid (Finset α)

Finset α is a Monoid under pointwise operations if α is.

abbrev Finset.nsmul_mem_nsmul.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

theorem Finset.nsmul_mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} (ha : a ∈ s) (n : ℕ) : n • a ∈ n • s

theorem Finset.pow_mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} (ha : a ∈ s) (n : ℕ) : a ^ n ∈ s ^ n

theorem Finset.nsmul_subset_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {t : Finset α} (hst : s ⊆ t) (n : ℕ) : n • s ⊆ n • t

theorem Finset.pow_subset_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {t : Finset α} (hst : s ⊆ t) (n : ℕ) : s ^ n ⊆ t ^ n

theorem Finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {m : ℕ} {n : ℕ} (hs : 0 ∈ s) : m ≤ n → m • s ⊆ n • s

theorem Finset.pow_subset_pow_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {m : ℕ} {n : ℕ} (hs : 1 ∈ s) : m ≤ n → s ^ m ⊆ s ^ n

@[simp]

theorem Finset.coe_list_sum {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : List (Finset α)) : ↑(List.sum s) = List.sum (List.map Finset.toSet s)

@[simp]

theorem Finset.coe_list_prod {α : Type u_2} [DecidableEq α] [Monoid α] (s : List (Finset α)) : ↑(List.prod s) = List.prod (List.map Finset.toSet s)

theorem Finset.mem_sum_list_ofFn {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} : a ∈ List.sum (List.ofFn s) ↔ ∃ f, List.sum (List.ofFn fun i => ↑(f i)) = a

theorem Finset.mem_prod_list_ofFn {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} : a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a

theorem Finset.mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} {n : ℕ} : a ∈ n • s ↔ ∃ f, List.sum (List.ofFn fun i => ↑(f i)) = a

theorem Finset.mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a

@[simp]

theorem Finset.empty_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} (hn : n ≠ 0) : n • ∅ = ∅

@[simp]

theorem Finset.empty_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} (hn : n ≠ 0) : ∅ ^ n = ∅

theorem Finset.add_univ_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} [Fintype α] (hs : 0 ∈ s) : s + Finset.univ = Finset.univ

theorem Finset.mul_univ_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} [Fintype α] (hs : 1 ∈ s) : s * Finset.univ = Finset.univ

theorem Finset.univ_add_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {t : Finset α} [Fintype α] (ht : 0 ∈ t) : Finset.univ + t = Finset.univ

theorem Finset.univ_mul_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {t : Finset α} [Fintype α] (ht : 1 ∈ t) : Finset.univ * t = Finset.univ

@[simp]

theorem Finset.univ_add_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] [Fintype α] : Finset.univ + Finset.univ = Finset.univ

@[simp]

theorem Finset.univ_mul_univ {α : Type u_2} [DecidableEq α] [Monoid α] [Fintype α] : Finset.univ * Finset.univ = Finset.univ

@[simp]

theorem Finset.nsmul_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} [Fintype α] (hn : n ≠ 0) : n • Finset.univ = Finset.univ

@[simp]

theorem Finset.univ_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} [Fintype α] (hn : n ≠ 0) : Finset.univ ^ n = Finset.univ

theorem IsAddUnit.finset {α : Type u_2} [DecidableEq α] [AddMonoid α] {a : α} : IsAddUnit a → IsAddUnit {a}

theorem IsUnit.finset {α : Type u_2} [DecidableEq α] [Monoid α] {a : α} : IsUnit a → IsUnit {a}

theorem Finset.addCommMonoid.proof_2 {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.addCommMonoid.proof_3 {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

theorem Finset.addCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] : ↑0 = 0

def Finset.addCommMonoid {α : Type u_2} [DecidableEq α] [AddCommMonoid α] : AddCommMonoid (Finset α)

Finset α is an AddCommMonoid under pointwise operations if α is.

def Finset.commMonoid {α : Type u_2} [DecidableEq α] [CommMonoid α] : CommMonoid (Finset α)

Finset α is a CommMonoid under pointwise operations if α is.

@[simp]

theorem Finset.coe_sum {α : Type u_2} [DecidableEq α] [AddCommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ι → Finset α) : ↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)

@[simp]

theorem Finset.coe_prod {α : Type u_2} [DecidableEq α] [CommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ι → Finset α) : ↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)

@[simp]

theorem Finset.coe_zsmul {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ℤ) : ↑(n • s) = n • ↑s

abbrev Finset.coe_zsmul.match_1 (motive : ℤ → Prop) : (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

@[simp]

theorem Finset.coe_zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] (s : Finset α) (n : ℤ) : ↑(s ^ n) = ↑s ^ n

theorem Finset.add_eq_zero_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} {t : Finset α} : s + t = 0 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a + b = 0

theorem Finset.mul_eq_one_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} {t : Finset α} : s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

theorem Finset.subtractionMonoid.proof_4 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (t : Finset α) : ↑(s - t) = ↑s - ↑t

def Finset.subtractionMonoid {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] : SubtractionMonoid (Finset α)

Finset α is a subtraction monoid under pointwise operations if α is.

theorem Finset.subtractionMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] : ↑0 = 0

theorem Finset.subtractionMonoid.proof_3 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) : ↑(-s) = -↑s

theorem Finset.subtractionMonoid.proof_2 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

theorem Finset.subtractionMonoid.proof_6 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ℤ) : ↑(n • s) = n • ↑s

theorem Finset.subtractionMonoid.proof_5 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

def Finset.divisionMonoid {α : Type u_2} [DecidableEq α] [DivisionMonoid α] : DivisionMonoid (Finset α)

Finset α is a division monoid under pointwise operations if α is.

@[simp]

theorem Finset.isAddUnit_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} : IsAddUnit s ↔ ∃ a, s = {a} ∧ IsAddUnit a

@[simp]

theorem Finset.isUnit_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} : IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

@[simp]

theorem Finset.isAddUnit_coe {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} : IsAddUnit ↑s ↔ IsAddUnit s

@[simp]

theorem Finset.isUnit_coe {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} : IsUnit ↑s ↔ IsUnit s

theorem Finset.subtractionCommMonoid.proof_1 {α : Type u_1} [SubtractionCommMonoid α] : ↑0 = 0

theorem Finset.subtractionCommMonoid.proof_6 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ℤ) : ↑(n • s) = n • ↑s

theorem Finset.subtractionCommMonoid.proof_3 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) : ↑(-s) = -↑s

theorem Finset.subtractionCommMonoid.proof_4 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (t : Finset α) : ↑(s - t) = ↑s - ↑t

def Finset.subtractionCommMonoid {α : Type u_2} [DecidableEq α] [SubtractionCommMonoid α] : SubtractionCommMonoid (Finset α)

Finset α is a commutative subtraction monoid under pointwise operations if α is.

theorem Finset.subtractionCommMonoid.proof_5 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

theorem Finset.subtractionCommMonoid.proof_2 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

def Finset.divisionCommMonoid {α : Type u_2} [DecidableEq α] [DivisionCommMonoid α] : DivisionCommMonoid (Finset α)

Finset α is a commutative division monoid under pointwise operations if α is.

def Finset.distribNeg {α : Type u_2} [DecidableEq α] [Mul α] [HasDistribNeg α] : HasDistribNeg (Finset α)

Finset α has distributive negation if α has.

Note that Finset α is not a Distrib because s * t + s * u has cross terms that s * (t + u) lacks.

-- {10, 16, 18, 20, 8, 9}
#eval {1, 2} * ({3, 4} + {5, 6} : Finset ℕ)

-- {10, 11, 12, 13, 14, 15, 16, 18, 20, 8, 9}
#eval ({1, 2} : Finset ℕ) * {3, 4} + {1, 2} * {5, 6}

theorem Finset.mul_add_subset {α : Type u_2} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) : s * (t + u) ⊆ s * t + s * u

theorem Finset.add_mul_subset {α : Type u_2} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) : (s + t) * u ⊆ s * u + t * u

Note that Finset is not a MulZeroClass because 0 * ∅ ≠ 0.

theorem Finset.mul_zero_subset {α : Type u_2} [DecidableEq α] [MulZeroClass α] (s : Finset α) : s * 0 ⊆ 0

theorem Finset.zero_mul_subset {α : Type u_2} [DecidableEq α] [MulZeroClass α] (s : Finset α) : 0 * s ⊆ 0

theorem Finset.Nonempty.mul_zero {α : Type u_2} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : Finset.Nonempty s) : s * 0 = 0

theorem Finset.Nonempty.zero_mul {α : Type u_2} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : Finset.Nonempty s) : 0 * s = 0

Note that Finset is not a Group because s / s ≠ 1 in general.

@[simp]

theorem Finset.zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} {t : Finset α} : 0 ∈ s - t ↔ ¬Disjoint s t

@[simp]

theorem Finset.one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} {t : Finset α} : 1 ∈ s / t ↔ ¬Disjoint s t

theorem Finset.not_zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} {t : Finset α} : ¬0 ∈ s - t ↔ Disjoint s t

theorem Finset.not_one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} {t : Finset α} : ¬1 ∈ s / t ↔ Disjoint s t

theorem Finset.Nonempty.zero_mem_sub {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} (h : Finset.Nonempty s) : 0 ∈ s - s

abbrev Finset.Nonempty.zero_mem_sub.match_1 {α : Type u_1} {s : Finset α} (motive : Finset.Nonempty s → Prop) : (h : Finset.Nonempty s) → ((a : α) → (ha : a ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive h

theorem Finset.Nonempty.one_mem_div {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} (h : Finset.Nonempty s) : 1 ∈ s / s

theorem Finset.isAddUnit_singleton {α : Type u_2} [DecidableEq α] [AddGroup α] (a : α) : IsAddUnit {a}

theorem Finset.isUnit_singleton {α : Type u_2} [DecidableEq α] [Group α] (a : α) : IsUnit {a}

theorem Finset.isUnit_iff_singleton {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} : IsUnit s ↔ ∃ a, s = {a}

@[simp]

theorem Finset.isUnit_iff_singleton_aux {α : Type u_2} [Group α] {s : Finset α} : (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}

@[simp]

theorem Finset.image_add_left {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} : Finset.image (fun b => a + b) t = Finset.preimage t (fun b => -a + b) (_ : Set.InjOn ((fun x x_1 => x + x_1) (-a)) ((fun b => -a + b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_mul_left {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} : Finset.image (fun b => a * b) t = Finset.preimage t (fun b => a⁻¹ * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun b => a⁻¹ * b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_add_right {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : Finset.image (fun x => x + b) t = Finset.preimage t (fun x => x + -b) (_ : Set.InjOn (fun x => x + -b) ((fun x => x + -b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_mul_right {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} : Finset.image (fun x => x * b) t = Finset.preimage t (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑t))

theorem Finset.image_add_left' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} : Finset.image (fun b => -a + b) t = Finset.preimage t (fun b => a + b) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun b => a + b) ⁻¹' ↑t))

theorem Finset.image_mul_left' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} : Finset.image (fun b => a⁻¹ * b) t = Finset.preimage t (fun b => a * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun b => a * b) ⁻¹' ↑t))

theorem Finset.image_add_right' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : Finset.image (fun x => x + -b) t = Finset.preimage t (fun x => x + b) (_ : Set.InjOn (fun x => x + b) ((fun x => x + b) ⁻¹' ↑t))

theorem Finset.image_mul_right' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} : Finset.image (fun x => x * b⁻¹) t = Finset.preimage t (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑t))

theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (f : F) {s : Finset α} {t : Finset α} : Finset.image (↑f) (s / t) = Finset.image (↑f) s / Finset.image (↑f) t

theorem Finset.div_zero_subset {α : Type u_2} [DecidableEq α] [GroupWithZero α] (s : Finset α) : s / 0 ⊆ 0

theorem Finset.zero_div_subset {α : Type u_2} [DecidableEq α] [GroupWithZero α] (s : Finset α) : 0 / s ⊆ 0

theorem Finset.Nonempty.div_zero {α : Type u_2} [DecidableEq α] [GroupWithZero α] {s : Finset α} (hs : Finset.Nonempty s) : s / 0 = 0

theorem Finset.Nonempty.zero_div {α : Type u_2} [DecidableEq α] [GroupWithZero α] {s : Finset α} (hs : Finset.Nonempty s) : 0 / s = 0

@[simp]

theorem Finset.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : Finset.preimage {b} ((fun x x_1 => x + x_1) a) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun x x_1 => x + x_1) a ⁻¹' ↑{b})) = {-a + b}

@[simp]

theorem Finset.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} : Finset.preimage {b} ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) = {a⁻¹ * b}

@[simp]

theorem Finset.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : Finset.preimage {b} (fun x => x + a) (_ : Set.InjOn (fun x => x + a) ((fun x => x + a) ⁻¹' ↑{b})) = {b + -a}

@[simp]

theorem Finset.preimage_mul_right_singleton {α : Type u_2} [Group α] {a : α} {b : α} : Finset.preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}

@[simp]

theorem Finset.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} : Finset.preimage 0 ((fun x x_1 => x + x_1) a) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun x x_1 => x + x_1) a ⁻¹' ↑0)) = {-a}

@[simp]

theorem Finset.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} : Finset.preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑1)) = {a⁻¹}

@[simp]

theorem Finset.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} : Finset.preimage 0 (fun x => x + b) (_ : Set.InjOn (fun x => x + b) ((fun x => x + b) ⁻¹' ↑0)) = {-b}

@[simp]

theorem Finset.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} : Finset.preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑1)) = {b⁻¹}

theorem Finset.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} : Finset.preimage 0 ((fun x x_1 => x + x_1) (-a)) (_ : Set.InjOn ((fun x x_1 => x + x_1) (-a)) ((fun x x_1 => x + x_1) (-a) ⁻¹' ↑0)) = {a}

theorem Finset.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} : Finset.preimage 1 ((fun x x_1 => x * x_1) a⁻¹) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a⁻¹ ⁻¹' ↑1)) = {a}

theorem Finset.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} : Finset.preimage 0 (fun x => x + -b) (_ : Set.InjOn (fun x => x + -b) ((fun x => x + -b) ⁻¹' ↑0)) = {b}

theorem Finset.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} : Finset.preimage 1 (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑1)) = {b}

Scalar addition/multiplication of finsets

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem Finset.coe_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) : ↑(s • t) = ↑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.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_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.card (s +ᵥ t) ≤ Finset.card s • Finset.card t

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : s • t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {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₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {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₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq α] : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Finset.subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {u : Finset β} {s : Set α} {t : Set β} : ↑u ⊆ s +ᵥ t → ∃ s' t', ↑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'.

theorem Finset.subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {u : Finset β} {s : Set α} {t : Set β} : ↑u ⊆ s • t → ∃ s' t', ↑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'.

Scalar subtraction of finsets

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

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

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

@[simp]

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

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

@[simp]

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

theorem Finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {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 : Finset β} {t : Finset β} : Finset.card (s -ᵥ t) ≤ Finset.card s * Finset.card t

@[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 : Finset β} {t : Finset β} : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

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

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

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

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

@[simp]

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

theorem Finset.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {t : Finset β} (a : β) : {a} -ᵥ t = Finset.image ((fun x x_1 => x -ᵥ x_1) a) 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₁ : Finset β} {s₂ : Finset β} {t₁ : Finset β} {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 : Finset β} {t₁ : Finset β} {t₂ : Finset β} : t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂

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

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

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

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

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

theorem Finset.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t₁ : Finset β} {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 : Set β} {t : Set β} : ↑u ⊆ s -ᵥ t → ∃ s' t', ↑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'.

Translation/scaling of finsets

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