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)