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.

Equations

• Finset.zero = { zero := {0} }

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

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

Equations

• Finset.one = { one := {1} }

@[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.coe_eq_zero {α : Type u_2} [Zero α] {s : Finset α} : ↑s = 0 ↔ s = 0

@[simp]

theorem Finset.coe_eq_one {α : Type u_2} [One α] {s : Finset α} : ↑s = 1 ↔ s = 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

@[simp]

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

@[simp]

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 : s.Nonempty) : s ⊆ 0 ↔ s = 0

theorem Finset.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Finset α} (h : s.Nonempty) : 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.

Equations

• Finset.singletonZeroHom = { toFun := singleton, map_zero' := ⋯ }

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

The singleton operation as a OneHom.

Equations

• Finset.singletonOneHom = { toFun := singleton, map_one' := ⋯ }

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

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

Lift a ZeroHom to Finset via image

Equations

• Finset.imageZeroHom f = { toFun := Finset.image ⇑f, map_zero' := ⋯ }

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

@[simp]

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

@[simp]

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

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

Lift a OneHom to Finset via image.

Equations

• Finset.imageOneHom f = { toFun := Finset.image ⇑f, map_one' := ⋯ }

@[simp]

theorem Finset.sup_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeSup β] [OrderBot β] (f : α → β) : Finset.sup 0 f = f 0

@[simp]

theorem Finset.sup_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeSup β] [OrderBot β] (f : α → β) : Finset.sup 1 f = f 1

@[simp]

theorem Finset.sup'_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeSup β] (f : α → β) : Finset.sup' 0 ⋯ f = f 0

@[simp]

theorem Finset.sup'_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeSup β] (f : α → β) : Finset.sup' 1 ⋯ f = f 1

@[simp]

theorem Finset.inf_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeInf β] [OrderTop β] (f : α → β) : Finset.inf 0 f = f 0

@[simp]

theorem Finset.inf_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeInf β] [OrderTop β] (f : α → β) : Finset.inf 1 f = f 1

@[simp]

theorem Finset.inf'_zero {α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeInf β] (f : α → β) : Finset.inf' 0 ⋯ f = f 0

@[simp]

theorem Finset.inf'_one {α : Type u_2} {β : Type u_3} [One α] [SemilatticeInf β] (f : α → β) : Finset.inf' 1 ⋯ f = f 1

@[simp]

theorem Finset.max_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.max 0 = 0

@[simp]

theorem Finset.max_one {α : Type u_2} [One α] [LinearOrder α] : Finset.max 1 = 1

@[simp]

theorem Finset.min_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.min 0 = 0

@[simp]

theorem Finset.min_one {α : Type u_2} [One α] [LinearOrder α] : Finset.min 1 = 1

@[simp]

theorem Finset.max'_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.max' 0 ⋯ = 0

@[simp]

theorem Finset.max'_one {α : Type u_2} [One α] [LinearOrder α] : Finset.max' 1 ⋯ = 1

@[simp]

theorem Finset.min'_zero {α : Type u_2} [Zero α] [LinearOrder α] : Finset.min' 0 ⋯ = 0

@[simp]

theorem Finset.min'_one {α : Type u_2} [One α] [LinearOrder α] : Finset.min' 1 ⋯ = 1

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.

Equations

• Finset.neg = { neg := Finset.image Neg.neg }

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.

Equations

• Finset.inv = { inv := Finset.image Inv.inv }

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 ∈ s, -y = x

theorem Finset.mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {x : α} : x ∈ s⁻¹ ↔ ∃ 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 α} : (-s).card ≤ s.card

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

@[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 α} : (-s).Nonempty ↔ s.Nonempty

@[simp]

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

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

Alias of the forward direction of Finset.inv_nonempty_iff.

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

Alias of the reverse direction of Finset.inv_nonempty_iff.

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

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

@[simp]

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

@[simp]

theorem Finset.inv_eq_empty {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : s⁻¹ = ∅ ↔ 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.sup_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : (-s).sup f = s.sup fun (x : α) => f (-x)

@[simp]

theorem Finset.sup_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : s⁻¹.sup f = s.sup fun (x : α) => f x⁻¹

@[simp]

theorem Finset.sup'_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeSup β] {s : Finset α} (hs : (-s).Nonempty) (f : α → β) : (-s).sup' hs f = s.sup' ⋯ fun (x : α) => f (-x)

@[simp]

theorem Finset.sup'_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : s⁻¹.sup' hs f = s.sup' ⋯ fun (x : α) => f x⁻¹

@[simp]

theorem Finset.inf_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : (-s).inf f = s.inf fun (x : α) => f (-x)

@[simp]

theorem Finset.inf_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : s⁻¹.inf f = s.inf fun (x : α) => f x⁻¹

@[simp]

theorem Finset.inf'_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeInf β] {s : Finset α} (hs : (-s).Nonempty) (f : α → β) : (-s).inf' hs f = s.inf' ⋯ fun (x : α) => f (-x)

@[simp]

theorem Finset.inf'_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeInf β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : s⁻¹.inf' hs f = s.inf' ⋯ fun (x : α) => f x⁻¹

theorem Finset.image_op_neg {α : Type u_2} [DecidableEq α] [Neg α] (s : Finset α) : Finset.image AddOpposite.op (-s) = -Finset.image AddOpposite.op s

theorem Finset.image_op_inv {α : Type u_2} [DecidableEq α] [Inv α] (s : Finset α) : Finset.image MulOpposite.op s⁻¹ = (Finset.image MulOpposite.op s)⁻¹

@[simp]

theorem Finset.mem_neg' {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] {s : Finset α} {a : α} : a ∈ -s ↔ -a ∈ s

@[simp]

theorem Finset.mem_inv' {α : Type u_2} [DecidableEq α] [InvolutiveInv α] {s : Finset α} {a : α} : a ∈ s⁻¹ ↔ 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 α) : (-s).card = s.card

@[simp]

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

@[simp]

theorem Finset.dens_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] [Fintype α] (s : Finset α) : (-s).dens = s.dens

@[simp]

theorem Finset.dens_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] [Fintype α] (s : Finset α) : s⁻¹.dens = s.dens

@[simp]

theorem Finset.preimage_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) : s.preimage (fun (x : α) => -x) ⋯ = -s

@[simp]

theorem Finset.preimage_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : s.preimage (fun (x : α) => x⁻¹) ⋯ = s⁻¹

@[simp]

theorem Finset.neg_univ {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] [Fintype α] : -Finset.univ = Finset.univ

@[simp]

theorem Finset.inv_univ {α : Type u_2} [DecidableEq α] [InvolutiveInv α] [Fintype α] : Finset.univ⁻¹ = Finset.univ

@[simp]

theorem Finset.neg_inter {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) (t : Finset α) : -(s ∩ t) = -s ∩ -t

@[simp]

theorem Finset.inv_inter {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) (t : Finset α) : (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

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.

Equations

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

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.

Equations

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

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

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

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

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

theorem Finset.mem_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {x : α} : x ∈ s + t ↔ ∃ 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 ∈ 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 α} : (s + t).card ≤ s.card * t.card

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

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

theorem Finset.card_mul_iff {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : (s * t).card = s.card * t.card ↔ Set.InjOn (fun (p : α × α) => p.1 * p.2) (↑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 α} : (s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

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

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

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

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

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

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

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

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 : α) => a + x) s

theorem Finset.singleton_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} (a : α) : {a} * s = Finset.image (fun (x : α) => a * x) 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 ∈ s, ∀ 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 ∈ s, ∀ 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' : Finset α) (t' : Finset α), ↑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' : Finset α) (t' : Finset α), ↑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 α] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) {s : Finset α} {t : Finset α} [DecidableEq β] : 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 α] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) {s : Finset α} {t : Finset α} [DecidableEq β] : Finset.image (⇑f) (s * t) = Finset.image (⇑f) s * Finset.image (⇑f) t

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

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

The singleton operation as an AddHom.

Equations

• Finset.singletonAddHom = { toFun := singleton, map_add' := ⋯ }

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

The singleton operation as a MulHom.

Equations

• Finset.singletonMulHom = { toFun := singleton, map_mul' := ⋯ }

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

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

Lift an AddHom to Finset via image

Equations

• Finset.imageAddHom f = { toFun := Finset.image ⇑f, map_add' := ⋯ }

@[simp]

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

@[simp]

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

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

Lift a MulHom to Finset via image.

Equations

• Finset.imageMulHom f = { toFun := Finset.image ⇑f, map_mul' := ⋯ }

@[simp]

theorem Finset.sup_add_le {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : (s + t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a

@[simp]

theorem Finset.sup_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : (s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a

theorem Finset.sup_add_left {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s + t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x + x_1)

theorem Finset.sup_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s * t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x * x_1)

theorem Finset.sup_add_right {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s + t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x + y)

theorem Finset.sup_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s * t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x * y)

@[simp]

theorem Finset.le_inf_add {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : a ≤ (s + t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x + y)

@[simp]

theorem Finset.le_inf_mul {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : a ≤ (s * t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)

theorem Finset.inf_add_left {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s + t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x + x_1)

theorem Finset.inf_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s * t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x * x_1)

theorem Finset.inf_add_right {α : Type u_2} [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s + t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x + y)

theorem Finset.inf_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_5} [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s * t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x * y)

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.

Equations

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

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.

Equations

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

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

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

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

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

theorem Finset.mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {a : α} : a ∈ s - t ↔ ∃ 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 ∈ 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 α} : (s - t).card ≤ s.card * t.card

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

@[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 α} : (s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

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

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

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

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

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

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

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

@[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 : α) => a - x) s

@[simp]

theorem Finset.singleton_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) : {a} / s = Finset.image (fun (x : α) => a / x) 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 ∈ s, ∀ 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 ∈ s, ∀ 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' : Finset α) (t' : Finset α), ↑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' : Finset α) (t' : Finset α), ↑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'.

@[simp]

theorem Finset.sup_sub_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : (s - t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x - y) ≤ a

@[simp]

theorem Finset.sup_div_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : (s / t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a

theorem Finset.sup_sub_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s - t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x - x_1)

theorem Finset.sup_div_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s / t).sup f = s.sup fun (x : α) => t.sup fun (x_1 : α) => f (x / x_1)

theorem Finset.sup_sub_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s - t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x - y)

theorem Finset.sup_div_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) : (s / t).sup f = t.sup fun (y : α) => s.sup fun (x : α) => f (x / y)

@[simp]

theorem Finset.le_inf_sub {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : a ≤ (s - t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x - y)

@[simp]

theorem Finset.le_inf_div {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} : a ≤ (s / t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y)

theorem Finset.inf_sub_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s - t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x - x_1)

theorem Finset.inf_div_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s / t).inf f = s.inf fun (x : α) => t.inf fun (x_1 : α) => f (x / x_1)

theorem Finset.inf_sub_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s - t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x - y)

theorem Finset.inf_div_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) : (s / t).inf f = t.inf fun (y : α) => s.inf fun (x : α) => f (x / y)

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

Equations

• Finset.nsmul = { smul := nsmulRec }

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

Equations

• Finset.npow = { pow := fun (s : Finset α) (n : ℕ) => npowRec n s }

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

Equations

• Finset.zsmul = { smul := zsmulRec }

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

Equations

• Finset.zpow = { pow := fun (s : Finset α) (n : ℤ) => zpowRec npowRec n s }

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

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

Equations

• Finset.addSemigroup = Function.Injective.addSemigroup Finset.toSet ⋯ ⋯

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

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

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

Equations

• Finset.semigroup = Function.Injective.semigroup Finset.toSet ⋯ ⋯

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.

Equations

• Finset.addCommSemigroup = Function.Injective.addCommSemigroup Finset.toSet ⋯ ⋯

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

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

Equations

• Finset.commSemigroup = Function.Injective.commSemigroup Finset.toSet ⋯ ⋯

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

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

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

Equations

• Finset.addZeroClass = Function.Injective.addZeroClass Finset.toSet ⋯ ⋯ ⋯

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

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

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

Equations

• Finset.mulOneClass = Function.Injective.mulOneClass Finset.toSet ⋯ ⋯ ⋯

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 : α) : Finset.singletonAddHom.toFun (x + y) = Finset.singletonAddHom.toFun x + Finset.singletonAddHom.toFun y

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

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

The singleton operation as an AddMonoidHom.

Equations

• Finset.singletonAddMonoidHom = { toFun := Finset.singletonAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }

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

The singleton operation as a MonoidHom.

Equations

• Finset.singletonMonoidHom = { toFun := Finset.singletonMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }

@[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_1 {α : Type u_1} [AddZeroClass α] : ↑0 = 0

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

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

The coercion from Finset to set as an AddMonoidHom.

Equations

• Finset.coeAddMonoidHom = { toFun := CoeTC.coe, map_zero' := ⋯, map_add' := ⋯ }

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

The coercion from Finset to Set as a MonoidHom.

Equations

• Finset.coeMonoidHom = { toFun := CoeTC.coe, map_one' := ⋯, map_mul' := ⋯ }

@[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 β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) : (Finset.imageZeroHom f).toFun 0 = 0

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

Lift an add_monoid_hom to Finset via image

Equations

• Finset.imageAddMonoidHom f = { toFun := (Finset.imageAddHom f).toFun, map_zero' := ⋯, map_add' := ⋯ }

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

@[simp]

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

@[simp]

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

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

Lift a MonoidHom to Finset via image.

Equations

• Finset.imageMonoidHom f = { toFun := (Finset.imageMulHom f).toFun, map_one' := ⋯, map_mul' := ⋯ }

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

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

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

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

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

Equations

• Finset.addMonoid = Function.Injective.addMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯

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

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

Equations

• Finset.monoid = Function.Injective.monoid Finset.toSet ⋯ ⋯ ⋯ ⋯

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 α)) : ↑s.sum = (List.map Finset.toSet s).sum

@[simp]

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

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

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

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

theorem Finset.mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ (f : Fin n → { x : α // x ∈ s }), (List.ofFn fun (i : Fin n) => ↑(f i)).prod = 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_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.

Equations

• Finset.addCommMonoid = Function.Injective.addCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯

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

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

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

Equations

• Finset.commMonoid = Function.Injective.commMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[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_5 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ℕ) : ↑(n • s) = n • ↑s

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.

Equations

• Finset.subtractionMonoid = Function.Injective.subtractionMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

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

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

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

Equations

• Finset.divisionMonoid = Function.Injective.divisionMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

@[simp]

theorem Finset.univ_sub_univ {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] [Fintype α] : Finset.univ - Finset.univ = Finset.univ

@[simp]

theorem Finset.univ_div_univ {α : Type u_2} [DecidableEq α] [DivisionMonoid α] [Fintype α] : Finset.univ / Finset.univ = Finset.univ

theorem Finset.subset_sub_left {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} {t : Finset α} (ht : 0 ∈ t) : s ⊆ s - t

theorem Finset.subset_div_left {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} {t : Finset α} (ht : 1 ∈ t) : s ⊆ s / t

theorem Finset.neg_subset_sub_right {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} {t : Finset α} (hs : 0 ∈ s) : -t ⊆ s - t

theorem Finset.inv_subset_div_right {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} {t : Finset α} (hs : 1 ∈ s) : t⁻¹ ⊆ s / t

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

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

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

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

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

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

Equations

• Finset.subtractionCommMonoid = Function.Injective.subtractionCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

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

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

Equations

• Finset.divisionCommMonoid = Function.Injective.divisionCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Finset α has distributive negation if α has.

Equations

• Finset.distribNeg = Function.Injective.hasDistribNeg Finset.toSet ⋯ ⋯ ⋯

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 : s.Nonempty) : s * 0 = 0

theorem Finset.Nonempty.zero_mul {α : Type u_2} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : s.Nonempty) : 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 : s.Nonempty) : 0 ∈ s - s

theorem Finset.Nonempty.one_mem_div {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} (h : s.Nonempty) : 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_5} [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 = t.preimage (fun (b : α) => -a + b) ⋯

@[simp]

theorem Finset.image_mul_left {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} : Finset.image (fun (b : α) => a * b) t = t.preimage (fun (b : α) => a⁻¹ * b) ⋯

@[simp]

theorem Finset.image_add_right {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : Finset.image (fun (x : α) => x + b) t = t.preimage (fun (x : α) => x + -b) ⋯

@[simp]

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

theorem Finset.image_add_left' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} : Finset.image (fun (b : α) => -a + b) t = t.preimage (fun (b : α) => a + b) ⋯

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

theorem Finset.image_add_right' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} : Finset.image (fun (x : α) => x + -b) t = t.preimage (fun (x : α) => x + b) ⋯

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

theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [FunLike F α β] [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 : s.Nonempty) : s / 0 = 0

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

@[simp]

theorem Finset.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : {b}.preimage (fun (x : α) => a + x) ⋯ = {-a + b}

@[simp]

theorem Finset.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} : {b}.preimage (fun (x : α) => a * x) ⋯ = {a⁻¹ * b}

@[simp]

theorem Finset.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : {b}.preimage (fun (x : α) => x + a) ⋯ = {b + -a}

@[simp]

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

@[simp]

theorem Finset.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} : Finset.preimage 0 (fun (x : α) => a + x) ⋯ = {-a}

@[simp]

theorem Finset.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} : Finset.preimage 1 (fun (x : α) => a * x) ⋯ = {a⁻¹}

@[simp]

theorem Finset.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} : Finset.preimage 0 (fun (x : α) => x + b) ⋯ = {-b}

@[simp]

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

theorem Finset.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} : Finset.preimage 0 (fun (x : α) => -a + x) ⋯ = {a}

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

theorem Finset.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} : Finset.preimage 0 (fun (x : α) => x + -b) ⋯ = {b}

theorem Finset.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} : Finset.preimage 1 (fun (x : α) => x * b⁻¹) ⋯ = {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}.

Equations

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

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 }

theorem Finset.vadd_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : s +ᵥ t = Finset.image (fun (p : α × β) => p.1 +ᵥ p.2) (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.1 • p.2) (s ×ˢ t)

theorem Finset.image_vadd_product {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.image (fun (x : α × β) => x.1 +ᵥ x.2) (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.1 • x.2) (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 ∈ 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 ∈ 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 β} : (s +ᵥ t).card ≤ s.card • t.card

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

@[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 β} : (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

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

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

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

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

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

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

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

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 ∈ s, ∀ 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 ∈ s, ∀ 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' : 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'.

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

Scalar subtraction of finsets

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

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

Equations

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

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

@[simp]

theorem Finset.image_vsub_product {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} : Finset.image₂ (fun (x1 x2 : β) => x1 -ᵥ x2) 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 ∈ 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 β} : (s -ᵥ t).card ≤ s.card * t.card

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem Finset.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} (b : β) : s -ᵥ {b} = 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 : β) => a -ᵥ x) t

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

theorem Finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ : 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 ∈ s, ∀ 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' : 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'.

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

Equations

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

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 }

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

instance Finset.vaddCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.smulCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.smulCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.smulCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Finset α) β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Finset α) (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Finset α) (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Finset α) (Finset β) (Finset γ)

Equations

• ⋯ = ⋯

instance Finset.isCentralVAdd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Finset β)

Equations

• ⋯ = ⋯

instance Finset.isCentralScalar {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Finset β)

Equations

• ⋯ = ⋯

theorem Finset.addAction.proof_2 {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] : ∀ (x x_1 : Finset α) (x_2 : Finset β), Finset.image₂ (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) (Finset.image₂ (fun (x1 x2 : α) => x1 + x2) x x_1) x_2 = Finset.image₂ (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) x (Finset.image₂ (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) x_1 x_2)

def Finset.addAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] : AddAction (Finset α) (Finset β)

An additive action of an additive monoid α on a type β gives an additive action of Finset α on Finset β

Equations

• Finset.addAction = AddAction.mk ⋯ ⋯

theorem Finset.addAction.proof_1 {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddMonoid α] [AddAction α β] (s : Finset β) : Finset.image₂ (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) {0} s = s

def Finset.mulAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [Monoid α] [MulAction α β] : MulAction (Finset α) (Finset β)

A multiplicative action of a monoid α on a type β gives a multiplicative action of Finset α on Finset β.

Equations

• Finset.mulAction = MulAction.mk ⋯ ⋯

theorem Finset.addActionFinset.proof_1 {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddMonoid α] [AddAction α β] (a : α) (s : Finset β) : ↑(a +ᵥ s) = a +ᵥ ↑s

def Finset.addActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddMonoid α] [AddAction α β] : AddAction α (Finset β)

An additive action of an additive monoid on a type β gives an additive action on Finset β.

Equations

• Finset.addActionFinset = Function.Injective.addAction Finset.toSet ⋯ ⋯

def Finset.mulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [MulAction α β] : MulAction α (Finset β)

A multiplicative action of a monoid on a type β gives a multiplicative action on Finset β.

Equations

• Finset.mulActionFinset = Function.Injective.mulAction Finset.toSet ⋯ ⋯

def Finset.smulZeroClassFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Zero β] [SMulZeroClass α β] : SMulZeroClass α (Finset β)

If scalar multiplication by elements of α sends (0 : β) to zero, then the same is true for (0 : Finset β).

Equations

• Finset.smulZeroClassFinset = Function.Injective.smulZeroClass { toFun := Finset.toSet, map_zero' := ⋯ } ⋯ ⋯

def Finset.distribSMulFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Finset β)

If the scalar multiplication (· • ·) : α → β → β is distributive, then so is (· • ·) : α → Finset β → Finset β.

Equations

• Finset.distribSMulFinset = Function.Injective.distribSMul Finset.coeAddMonoidHom ⋯ ⋯

def Finset.distribMulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Finset β)

A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Finset β.

Equations

• Finset.distribMulActionFinset = Function.Injective.distribMulAction Finset.coeAddMonoidHom ⋯ ⋯

def Finset.mulDistribMulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [Monoid β] [MulDistribMulAction α β] : MulDistribMulAction α (Finset β)

A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

Equations

• Finset.mulDistribMulActionFinset = Function.Injective.mulDistribMulAction Finset.coeMonoidHom ⋯ ⋯

instance Finset.instNoZeroDivisors {α : Type u_2} [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Finset α)

Equations

• ⋯ = ⋯

instance Finset.noZeroSMulDivisors {α : Type u_2} {β : Type u_3} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Finset α) (Finset β)

Equations

• ⋯ = ⋯

instance Finset.noZeroSMulDivisors_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Finset β)

Equations

• ⋯ = ⋯

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

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

theorem Finset.op_vadd_finset_subset_add {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t

theorem Finset.op_smul_finset_subset_mul {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ t → MulOpposite.op a • s ⊆ s * t

@[simp]

theorem Finset.biUnion_op_vadd_finset {α : Type u_2} [Add α] [DecidableEq α] (s : Finset α) (t : Finset α) : (t.biUnion fun (a : α) => AddOpposite.op a +ᵥ s) = s + t

@[simp]

theorem Finset.biUnion_op_smul_finset {α : Type u_2} [Mul α] [DecidableEq α] (s : Finset α) (t : Finset α) : (t.biUnion fun (a : α) => MulOpposite.op a • s) = s * t

theorem Finset.add_subset_iff_left {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u

theorem Finset.mul_subset_iff_left {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

theorem Finset.add_subset_iff_right {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u

theorem Finset.mul_subset_iff_right {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u

theorem Finset.op_vadd_finset_add_eq_add_vadd_finset {α : Type u_2} [AddSemigroup α] [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)

theorem Finset.op_smul_finset_mul_eq_mul_smul_finset {α : Type u_2} [Semigroup α] [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : MulOpposite.op a • s * t = s * a • t

theorem Finset.pairwiseDisjoint_vadd_iff {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {s : Set α} {t : Finset α} : (s.PairwiseDisjoint fun (x : α) => x +ᵥ t) ↔ Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ ↑t)

theorem Finset.pairwiseDisjoint_smul_iff {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] {s : Set α} {t : Finset α} : (s.PairwiseDisjoint fun (x : α) => x • t) ↔ Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ ↑t)

@[simp]

theorem Finset.card_singleton_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] (t : Finset α) (a : α) : ({a} + t).card = t.card

@[simp]

theorem Finset.card_singleton_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] (t : Finset α) (a : α) : ({a} * t).card = t.card

theorem Finset.singleton_add_inter {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : {a} + s ∩ t = ({a} + s) ∩ ({a} + t)

theorem Finset.singleton_mul_inter {α : Type u_2} [Mul α] [IsLeftCancelMul α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : {a} * (s ∩ t) = {a} * s ∩ ({a} * t)

theorem Finset.card_le_card_add_left {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] (t : Finset α) {s : Finset α} (hs : s.Nonempty) : t.card ≤ (s + t).card

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

theorem Finset.card_le_card_add_self {α : Type u_2} [Add α] [IsLeftCancelAdd α] [DecidableEq α] {s : Finset α} : s.card ≤ (s + s).card

The size of s + s is at least the size of s, version with left-cancellative addition. See card_le_card_add_self' for the version with right-cancellative addition.

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

The size of s * s is at least the size of s, version with left-cancellative multiplication. See card_le_card_mul_self' for the version with right-cancellative multiplication.

@[simp]

theorem Finset.card_add_singleton {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] (s : Finset α) (a : α) : (s + {a}).card = s.card

@[simp]

theorem Finset.card_mul_singleton {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] (s : Finset α) (a : α) : (s * {a}).card = s.card

theorem Finset.inter_add_singleton {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : s ∩ t + {a} = (s + {a}) ∩ (t + {a})

theorem Finset.inter_mul_singleton {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : s ∩ t * {a} = s * {a} ∩ (t * {a})

theorem Finset.card_le_card_add_right {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] (s : Finset α) {t : Finset α} (ht : t.Nonempty) : s.card ≤ (s + t).card

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

theorem Finset.card_le_card_add_self' {α : Type u_2} [Add α] [IsRightCancelAdd α] [DecidableEq α] {s : Finset α} : s.card ≤ (s + s).card

The size of s + s is at least the size of s, version with right-cancellative addition. See card_le_card_add_self for the version with left-cancellative addition.

theorem Finset.card_le_card_mul_self' {α : Type u_2} [Mul α] [IsRightCancelMul α] [DecidableEq α] {s : Finset α} : s.card ≤ (s * s).card

The size of s * s is at least the size of s, version with right-cancellative multiplication. See card_le_card_mul_self for the version with left-cancellative multiplication.

theorem Finset.card_le_card_sub_left {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} (hs : s.Nonempty) : t.card ≤ (s - t).card

theorem Finset.card_le_card_div_left {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} (hs : s.Nonempty) : t.card ≤ (s / t).card

theorem Finset.card_le_card_sub_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} (ht : t.Nonempty) : s.card ≤ (s - t).card

theorem Finset.card_le_card_div_right {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} (ht : t.Nonempty) : s.card ≤ (s / t).card

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

theorem Finset.card_le_card_div_self {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.card ≤ (s / s).card

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) → Finset.image f (a +ᵥ s) = a +ᵥ Finset.image f s

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) → Finset.image f (a • s) = a • Finset.image f s

theorem Finset.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (a : α) (s : Finset α) : Finset.image (⇑f) (a +ᵥ s) = f a +ᵥ Finset.image (⇑f) s

theorem Finset.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (a : α) (s : Finset α) : Finset.image (⇑f) (a • s) = f a • Finset.image (⇑f) s

@[simp]

theorem Finset.vadd_mem_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {b : β} (a : α) : a +ᵥ b ∈ a +ᵥ s ↔ b ∈ s

@[simp]

theorem Finset.smul_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {b : β} (a : α) : a • b ∈ a • s ↔ b ∈ s

theorem Finset.neg_vadd_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} : -a +ᵥ b ∈ s ↔ b ∈ a +ᵥ s

theorem Finset.inv_smul_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} : a⁻¹ • b ∈ s ↔ b ∈ a • s

theorem Finset.mem_neg_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} : b ∈ -a +ᵥ s ↔ a +ᵥ b ∈ s

theorem Finset.mem_inv_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} : b ∈ a⁻¹ • s ↔ a • b ∈ s

@[simp]

theorem Finset.vadd_finset_subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t

@[simp]

theorem Finset.smul_finset_subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : a • s ⊆ a • t ↔ s ⊆ t

theorem Finset.vadd_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : a +ᵥ s ⊆ t ↔ s ⊆ -a +ᵥ t

theorem Finset.smul_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : a • s ⊆ t ↔ s ⊆ a⁻¹ • t

theorem Finset.subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : s ⊆ a +ᵥ t ↔ -a +ᵥ s ⊆ t

theorem Finset.subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : s ⊆ a • t ↔ a⁻¹ • s ⊆ t

theorem Finset.vadd_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

theorem Finset.smul_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : a • (s ∩ t) = a • s ∩ a • t

theorem Finset.vadd_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)

theorem Finset.smul_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : a • (s \ t) = a • s \ a • t

theorem Finset.vadd_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} : a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)

theorem Finset.smul_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} : a • symmDiff s t = symmDiff (a • s) (a • t)

@[simp]

theorem Finset.vadd_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {a : α} [Fintype β] : a +ᵥ Finset.univ = Finset.univ

@[simp]

theorem Finset.smul_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {a : α} [Fintype β] : a • Finset.univ = Finset.univ

@[simp]

theorem Finset.vadd_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] [Fintype β] {s : Finset α} (hs : s.Nonempty) : s +ᵥ Finset.univ = Finset.univ

@[simp]

theorem Finset.smul_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] [Fintype β] {s : Finset α} (hs : s.Nonempty) : s • Finset.univ = Finset.univ

@[simp]

theorem Finset.card_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] (a : α) (s : Finset β) : (a +ᵥ s).card = s.card

@[simp]

theorem Finset.card_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] (a : α) (s : Finset β) : (a • s).card = s.card

@[simp]

theorem Finset.dens_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] [Fintype β] (a : α) (s : Finset β) : (a +ᵥ s).dens = s.dens

@[simp]

theorem Finset.dens_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] [Fintype β] (a : α) (s : Finset β) : (a • s).dens = s.dens

theorem Finset.card_dvd_card_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {t : Finset β} {s : Finset α} : ((fun (x : α) => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s +ᵥ t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s +ᵥ t.

theorem Finset.card_dvd_card_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {t : Finset β} {s : Finset α} : ((fun (x : α) => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s • t.

theorem Finset.card_dvd_card_add_left {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} : ((fun (b : α) => Finset.image (fun (a : α) => a + b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s + t).card

If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s + t.

theorem Finset.card_dvd_card_mul_left {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} : ((fun (b : α) => Finset.image (fun (a : α) => a * b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s * t).card

If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s * t.

theorem Finset.card_dvd_card_add_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} : ((fun (x : α) => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s + t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s + t.

theorem Finset.card_dvd_card_mul_right {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} : ((fun (x : α) => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s * t).card

If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s * t.

@[simp]

theorem Finset.neg_vadd_finset_distrib {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) (s : Finset α) : -(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s

@[simp]

theorem Finset.inv_smul_finset_distrib {α : Type u_2} [Group α] [DecidableEq α] (a : α) (s : Finset α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

theorem Finset.neg_op_vadd_finset_distrib {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) (s : Finset α) : -(AddOpposite.op a +ᵥ s) = -a +ᵥ -s

@[simp]

theorem Finset.inv_op_smul_finset_distrib {α : Type u_2} [Group α] [DecidableEq α] (a : α) (s : Finset α) : (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹

theorem Finset.smul_zero_subset {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] [DecidableEq β] (s : Finset α) : s • 0 ⊆ 0

theorem Finset.Nonempty.smul_zero {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] [DecidableEq β] {s : Finset α} (hs : s.Nonempty) : s • 0 = 0

theorem Finset.zero_mem_smul_finset {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] [DecidableEq β] {t : Finset β} {a : α} (h : 0 ∈ t) : 0 ∈ a • t

theorem Finset.zero_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] [DecidableEq β] {t : Finset β} {a : α} [Zero α] [NoZeroSMulDivisors α β] (ha : a ≠ 0) : 0 ∈ a • t ↔ 0 ∈ t

Note that we have neither SMulWithZero α (Finset β) nor SMulWithZero (Finset α) (Finset β) because 0 • ∅ ≠ 0.

theorem Finset.zero_smul_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] (t : Finset β) : 0 • t ⊆ 0

theorem Finset.Nonempty.zero_smul {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {t : Finset β} (ht : t.Nonempty) : 0 • t = 0

@[simp]

theorem Finset.zero_smul_finset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset β} (h : s.Nonempty) : 0 • s = 0

A nonempty set is scaled by zero to the singleton set containing zero.

theorem Finset.zero_smul_finset_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] (s : Finset β) : 0 • s ⊆ 0

theorem Finset.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset α} {t : Finset β} [NoZeroSMulDivisors α β] : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

@[simp]

theorem Finset.smul_mem_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a ≠ 0) : a • b ∈ a • s ↔ b ∈ s

theorem Finset.inv_smul_mem_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a ≠ 0) : a⁻¹ • b ∈ s ↔ b ∈ a • s

theorem Finset.mem_inv_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a ≠ 0) : b ∈ a⁻¹ • s ↔ a • b ∈ s

@[simp]

theorem Finset.smul_finset_subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t

theorem Finset.smul_finset_subset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • s ⊆ t ↔ s ⊆ a⁻¹ • t

theorem Finset.subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : s ⊆ a • t ↔ a⁻¹ • s ⊆ t

theorem Finset.smul_finset_inter₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t

theorem Finset.smul_finset_sdiff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t

theorem Finset.smul_finset_symmDiff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem Finset.smul_finset_univ₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {a : α} [Fintype β] (ha : a ≠ 0) : a • Finset.univ = Finset.univ

theorem Finset.smul_univ₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] [Fintype β] {s : Finset α} (hs : ¬s ⊆ 0) : s • Finset.univ = Finset.univ

theorem Finset.smul_univ₀' {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] [Fintype β] {s : Finset α} (hs : s.Nontrivial) : s • Finset.univ = Finset.univ

@[simp]

theorem Finset.inv_zero {α : Type u_2} [GroupWithZero α] [DecidableEq α] : 0⁻¹ = 0

@[simp]

theorem Finset.inv_smul_finset_distrib₀ {α : Type u_2} [GroupWithZero α] [DecidableEq α] (a : α) (s : Finset α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

theorem Finset.inv_op_smul_finset_distrib₀ {α : Type u_2} [GroupWithZero α] [DecidableEq α] (a : α) (s : Finset α) : (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹

@[simp]

theorem Finset.smul_finset_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] [DecidableEq β] (a : α) (t : Finset β) : a • -t = -(a • t)

@[simp]

theorem Finset.smul_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] [DecidableEq β] (s : Finset α) (t : Finset β) : s • -t = -(s • t)

@[simp]

theorem Finset.neg_smul_finset {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {t : Finset β} {a : α} : -a • t = -(a • t)

@[simp]

theorem Finset.neg_smul {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {s : Finset α} {t : Finset β} [DecidableEq α] : -s • t = -(s • t)

@[simp]

theorem Finset.sum_neg_index {α : Type u_2} [AddCommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ -s, f i = ∑ i ∈ s, f (-i)

@[simp]

theorem Finset.prod_inv_index {α : Type u_2} [CommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹

@[simp]

theorem Finset.prod_neg_index {α : Type u_2} [CommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ -s, f i = ∏ i ∈ s, f (-i)

@[simp]

theorem Finset.sum_inv_index {α : Type u_2} [AddCommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹

theorem Fintype.piFinset_vadd {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)) : (Fintype.piFinset fun (i : ι) => s i +ᵥ t i) = Fintype.piFinset s +ᵥ Fintype.piFinset t

theorem Fintype.piFinset_smul {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)) : (Fintype.piFinset fun (i : ι) => s i • t i) = Fintype.piFinset s • Fintype.piFinset t

theorem Fintype.piFinset_vadd_finset {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → VAdd (α i) (β i)] (a : (i : ι) → α i) (s : (i : ι) → Finset (β i)) : (Fintype.piFinset fun (i : ι) => a i +ᵥ s i) = a +ᵥ Fintype.piFinset s

theorem Fintype.piFinset_smul_finset {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul (α i) (β i)] (a : (i : ι) → α i) (s : (i : ι) → Finset (β i)) : (Fintype.piFinset fun (i : ι) => a i • s i) = a • Fintype.piFinset s

theorem Fintype.piFinset_add {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Add (α i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => s i + t i) = Fintype.piFinset s + Fintype.piFinset t

theorem Fintype.piFinset_mul {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Mul (α i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => s i * t i) = Fintype.piFinset s * Fintype.piFinset t

theorem Fintype.piFinset_sub {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Sub (α i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => s i - t i) = Fintype.piFinset s - Fintype.piFinset t

theorem Fintype.piFinset_div {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Div (α i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => s i / t i) = Fintype.piFinset s / Fintype.piFinset t

@[simp]

theorem Fintype.piFinset_neg {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Neg (α i)] (s : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => -s i) = -Fintype.piFinset s

@[simp]

theorem Fintype.piFinset_inv {ι : Type u_5} {α : ι → Type u_6} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Inv (α i)] (s : (i : ι) → Finset (α i)) : (Fintype.piFinset fun (i : ι) => (s i)⁻¹) = (Fintype.piFinset s)⁻¹

instance Set.instFintypeZero {α : Type u_2} [Zero α] : Fintype ↑0

Equations

• Set.instFintypeZero = Set.fintypeSingleton 0

instance Set.instFintypeOne {α : Type u_2} [One α] : Fintype ↑1

Equations

• Set.instFintypeOne = Set.fintypeSingleton 1

@[simp]

theorem Set.toFinset_zero {α : Type u_2} [Zero α] : Set.toFinset 0 = 0

@[simp]

theorem Set.toFinset_one {α : Type u_2} [One α] : Set.toFinset 1 = 1

@[simp]

theorem Set.Finite.toFinset_zero {α : Type u_2} [Zero α] (h : optParam (Set.Finite 0) ⋯) : Set.Finite.toFinset h = 0

@[simp]

theorem Set.Finite.toFinset_one {α : Type u_2} [One α] (h : optParam (Set.Finite 1) ⋯) : Set.Finite.toFinset h = 1

@[simp]

theorem Set.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] (s : Set α) (t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s + t)] : (s + t).toFinset = s.toFinset + t.toFinset

@[simp]

theorem Set.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Set α) (t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s * t)] : (s * t).toFinset = s.toFinset * t.toFinset

theorem Set.Finite.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] {s : Set α} {t : Set α} (hs : s.Finite) (ht : t.Finite) (hf : optParam (s + t).Finite ⋯) : Set.Finite.toFinset hf = hs.toFinset + ht.toFinset

theorem Set.Finite.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Set α} {t : Set α} (hs : s.Finite) (ht : t.Finite) (hf : optParam (s * t).Finite ⋯) : Set.Finite.toFinset hf = hs.toFinset * ht.toFinset

@[simp]

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

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

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

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

@[simp]

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

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

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

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

@[simp]

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

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

instance Nat.decidablePred_mem_vadd_set {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (a : ℕ) : DecidablePred fun (x : ℕ) => x ∈ a +ᵥ s

Equations

• a.decidablePred_mem_vadd_set n = decidable_of_iff' (a ≤ n ∧ n - a ∈ s) ⋯