Documentation

Mathlib.Data.Finset.Pointwise

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

Instances For

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

Instances For

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

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

0.Nonempty

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

1.Nonempty

@[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 α] :

0.card = 1

@[simp]

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

1.card = 1

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

ZeroHom α (Finset α)

The singleton operation as a ZeroHom.

Equations

Finset.singletonZeroHom = { toFun := singleton, map_zero' := (_ : {0} = 0) }

Instances For

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

OneHom α (Finset α)

The singleton operation as a OneHom.

Equations

Finset.singletonOneHom = { toFun := singleton, map_one' := (_ : {1} = 1) }

Instances For

@[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' := (_ : Finset.image (⇑f) 0 = 0) }

Instances For

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' := (_ : Finset.image (⇑f) 1 = 1) }

Instances For

@[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 (_ : 0.Nonempty) f = f 0

@[simp]

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

Finset.sup' 1 (_ : 1.Nonempty) 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 (_ : 0.Nonempty) f = f 0

@[simp]

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

Finset.inf' 1 (_ : 1.Nonempty) 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.Nonempty) = 0

@[simp]

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

Finset.max' 1 (_ : 1.Nonempty) = 1

@[simp]

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

Finset.min' 0 (_ : 0.Nonempty) = 0

@[simp]

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

Finset.min' 1 (_ : 1.Nonempty) = 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 }

Instances For

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 }

Instances For

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) :

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.of_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} :

(-s).Nonempty → s.Nonempty

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

s.Nonempty → (-s).Nonempty

theorem Finset.neg_subset_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {t : Finset α} (h : 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 : α → β) :

Finset.sup (-s) f = Finset.sup s fun (x : α) => f (-x)

@[simp]

theorem Finset.sup_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) :

Finset.sup s⁻¹ f = Finset.sup s fun (x : α) => f x⁻¹

@[simp]

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

Finset.sup' (-s) hs f = Finset.sup' s (_ : s.Nonempty) fun (x : α) => f (-x)

@[simp]

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

Finset.sup' s⁻¹ hs f = Finset.sup' s (_ : s.Nonempty) fun (x : α) => f x⁻¹

@[simp]

theorem Finset.inf_neg {α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) :

Finset.inf (-s) f = Finset.inf s fun (x : α) => f (-x)

@[simp]

theorem Finset.inf_inv {α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) :

Finset.inf s⁻¹ f = Finset.inf s fun (x : α) => f x⁻¹

@[simp]

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

Finset.inf' (-s) hs f = Finset.inf' s (_ : s.Nonempty) fun (x : α) => f (-x)

@[simp]

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

Finset.inf' s⁻¹ hs f = Finset.inf' s (_ : s.Nonempty) 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.preimage_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) :

Finset.preimage s (fun (x : α) => -x) (_ : Set.InjOn Neg.neg ((fun (x : α) => -x) ⁻¹' ↑s)) = -s

@[simp]

theorem Finset.preimage_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) :

Finset.preimage s (fun (x : α) => x⁻¹) (_ : Set.InjOn Inv.inv ((fun (x : α) => x⁻¹) ⁻¹' ↑s)) = 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

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 (x x_1 : α) => x + x_1 }

Instances For

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 (x x_1 : α) => x * x_1 }

Instances For

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 α) :

@[simp]

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

@[simp]

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

@[simp]

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

@[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 α] [DecidableEq β] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) {s : Finset α} {t : Finset α} :

Finset.image (⇑f) (s + t) = Finset.image (⇑f) s + Finset.image (⇑f) t

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

Finset.image (⇑f) (s * t) = Finset.image (⇑f) s * Finset.image (⇑f) t

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

AddHom α (Finset α)

The singleton operation as an AddHom.

Equations

Finset.singletonAddHom = { toFun := singleton, map_add' := (_ : ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}) }

Instances For

theorem Finset.singletonAddHom.proof_1 {α : Type u_1} [DecidableEq α] [Add α] :

∀ (x x_1 : α), {x + x_1} = {x} + {x_1}

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

α →ₙ* Finset α

The singleton operation as a MulHom.

Equations

Finset.singletonMulHom = { toFun := singleton, map_mul' := (_ : ∀ (x x_1 : α), {x * x_1} = {x} * {x_1}) }

Instances For

@[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 α] [DecidableEq β] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) :

AddHom (Finset α) (Finset β)

Lift an AddHom to Finset via image

Equations

Finset.imageAddHom f = { toFun := Finset.image ⇑f, map_add' := (_ : ∀ (x x_1 : Finset α), Finset.image (⇑f) (x + x_1) = Finset.image (⇑f) x + Finset.image (⇑f) x_1) }

Instances For

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

∀ (x x_1 : Finset α), Finset.image (⇑f) (x + x_1) = Finset.image (⇑f) x + Finset.image (⇑f) x_1

@[simp]

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

(Finset.imageAddHom f) s = Finset.image (⇑f) s

@[simp]

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

(Finset.imageMulHom f) s = Finset.image (⇑f) s

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

Finset α →ₙ* Finset β

Lift a MulHom to Finset via image.

Equations

Finset.imageMulHom f = { toFun := Finset.image ⇑f, map_mul' := (_ : ∀ (x x_1 : Finset α), Finset.image (⇑f) (x * x_1) = Finset.image (⇑f) x * Finset.image (⇑f) x_1) }

Instances For

@[simp]

theorem Finset.sup_add_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} :

Finset.sup (s + t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a

@[simp]

theorem Finset.sup_mul_le {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeSup β] [OrderBot β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} :

Finset.sup (s * t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a

theorem Finset.sup_add_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.sup (s + t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x + x_1)

theorem Finset.sup_mul_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.sup (s * t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x * x_1)

theorem Finset.sup_add_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.sup (s + t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x + y)

theorem Finset.sup_mul_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.sup (s * t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x * y)

@[simp]

theorem Finset.le_inf_add {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} :

a ≤ Finset.inf (s + t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x + y)

@[simp]

theorem Finset.le_inf_mul {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeInf β] [OrderTop β] {s : Finset α} {t : Finset α} {f : α → β} {a : β} :

a ≤ Finset.inf (s * t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)

theorem Finset.inf_add_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.inf (s + t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x + x_1)

theorem Finset.inf_mul_left {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.inf (s * t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x * x_1)

theorem Finset.inf_add_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Add α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.inf (s + t) f = Finset.inf t fun (y : α) => Finset.inf s fun (x : α) => f (x + y)

theorem Finset.inf_mul_right {α : Type u_2} {β : Type u_3} [DecidableEq α] [Mul α] [SemilatticeInf β] [OrderTop β] (s : Finset α) (t : Finset α) (f : α → β) :

Finset.inf (s * t) f = Finset.inf t fun (y : α) => Finset.inf s 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 (x x_1 : α) => x - x_1 }

Instances For

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 (x x_1 : α) => x / x_1 }

Instances For

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 α) :

@[simp]

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

@[simp]

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

@[simp]

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

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

Finset.sup (s - t) 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 : β} :

Finset.sup (s / t) 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 : α → β) :

Finset.sup (s - t) f = Finset.sup s fun (x : α) => Finset.sup t 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 : α → β) :

Finset.sup (s / t) f = Finset.sup s fun (x : α) => Finset.sup t 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 : α → β) :

Finset.sup (s - t) f = Finset.sup t fun (y : α) => Finset.sup s 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 : α → β) :

Finset.sup (s / t) f = Finset.sup t fun (y : α) => Finset.sup s 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 ≤ Finset.inf (s - t) 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 ≤ Finset.inf (s / t) 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 : α → β) :

Finset.inf (s - t) f = Finset.inf s fun (x : α) => Finset.inf t 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 : α → β) :

Finset.inf (s / t) f = Finset.inf s fun (x : α) => Finset.inf t 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 : α → β) :

Finset.inf (s - t) f = Finset.inf t fun (y : α) => Finset.inf s 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 : α → β) :

Finset.inf (s / t) f = Finset.inf t fun (y : α) => Finset.inf s 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 }

Instances For

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 }

Instances For

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 }

Instances For

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 n s }

Instances For

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

↑(s + t) = ↑s + ↑t

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

AddSemigroup (Finset α)

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

Equations

Finset.addSemigroup = Function.Injective.addSemigroup Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ↑{0} = {0}) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ↑{1} = {1}) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

Instances For

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

One or more equations did not get rendered due to their size.

Instances For

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

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

α →* Finset α

The singleton operation as a MonoidHom.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[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 = { toZeroHom := { toFun := CoeTC.coe, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t) }

Instances For

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

Finset α →* Set α

The coercion from Finset to Set as a MonoidHom.

Equations

Finset.coeMonoidHom = { toOneHom := { toFun := CoeTC.coe, map_one' := (_ : ↑1 = 1) }, map_mul' := (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t) }

Instances For

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

One or more equations did not get rendered due to their size.

Instances For

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

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

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

One or more equations did not get rendered due to their size.

Instances For

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

One or more equations did not get rendered due to their size.

Instances For

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

↑(s + t) = ↑s + ↑t

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

↑(n • s) = n • ↑s

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

Monoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

abbrev Finset.nsmul_mem_nsmul.match_1 (motive : ℕ → Prop) :

∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive (Nat.succ n)) → motive x

Equations

(_ : motive x) = (_ : motive x)

Instances For

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

n • a ∈ n • s

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

a ^ n ∈ s ^ n

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

n • s ⊆ n • t

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

s ^ n ⊆ t ^ n

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

m ≤ n → m • s ⊆ n • s

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

m ≤ n → s ^ m ⊆ s ^ n

@[simp]

theorem Finset.coe_list_sum {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : List (Finset α)) :

↑(List.sum s) = List.sum (List.map Finset.toSet s)

@[simp]

theorem Finset.coe_list_prod {α : Type u_2} [DecidableEq α] [Monoid α] (s : List (Finset α)) :

↑(List.prod s) = List.prod (List.map Finset.toSet s)

theorem Finset.mem_sum_list_ofFn {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} :

a ∈ List.sum (List.ofFn s) ↔ ∃ (f : (i : Fin n) → { x : α // x ∈ s i }), List.sum (List.ofFn fun (i : Fin n) => ↑(f i)) = a

theorem Finset.mem_prod_list_ofFn {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} {a : α} {s : Fin n → Finset α} :

a ∈ List.prod (List.ofFn s) ↔ ∃ (f : (i : Fin n) → { x : α // x ∈ s i }), List.prod (List.ofFn fun (i : Fin n) => ↑(f i)) = a

theorem Finset.mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} {n : ℕ} :

a ∈ n • s ↔ ∃ (f : Fin n → { x : α // x ∈ s }), List.sum (List.ofFn fun (i : Fin n) => ↑(f i)) = a

theorem Finset.mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : ℕ} :

a ∈ s ^ n ↔ ∃ (f : Fin n → { x : α // x ∈ s }), List.prod (List.ofFn fun (i : Fin n) => ↑(f i)) = a

@[simp]

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

n • ∅ = ∅

@[simp]

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

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

One or more equations did not get rendered due to their size.

Instances For

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

↑(n • s) = n • ↑s

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

↑(s + t) = ↑s + ↑t

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

CommMonoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Finset.coe_sum {α : Type u_2} [DecidableEq α] [AddCommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ι → Finset α) :

↑(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => ↑(f i)

@[simp]

theorem Finset.coe_prod {α : Type u_2} [DecidableEq α] [CommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ι → Finset α) :

↑(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ↑(f i)

@[simp]

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

↑(n • s) = n • ↑s

abbrev Finset.coe_zsmul.match_1 (motive : ℤ → Prop) :

∀ (x : ℤ), (∀ (n : ℕ), motive (Int.ofNat n)) → (∀ (n : ℕ), motive (Int.negSucc n)) → motive x

Equations

(_ : motive x) = (_ : motive x)

Instances For

@[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_1 {α : Type u_1} [SubtractionMonoid α] :

↑0 = 0

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

↑(n • s) = n • ↑s

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

↑(-s) = -↑s

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

↑(s - t) = ↑s - ↑t

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

↑(s + t) = ↑s + ↑t

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

↑(n • s) = n • ↑s

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

SubtractionMonoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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

DivisionMonoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[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.subtractionCommMonoid.proof_5 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ℕ) :

↑(n • s) = n • ↑s

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

↑(-s) = -↑s

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

SubtractionCommMonoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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

↑0 = 0

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

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

↑(s + t) = ↑s + ↑t

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

DivisionCommMonoid (Finset α)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (s : Finset α), ↑(-s) = -↑s) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

Instances For

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

abbrev Finset.Nonempty.zero_mem_sub.match_1 {α : Type u_1} {s : Finset α} (motive : s.Nonempty → Prop) :

∀ (h : s.Nonempty), (∀ (a : α) (ha : a ∈ s), motive (_ : ∃ (x : α), x ∈ s)) → motive h

Equations

(_ : motive h) = (_ : motive h)

Instances For

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 : α) :

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

theorem Finset.isUnit_iff_singleton {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} :

IsUnit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem Finset.isUnit_iff_singleton_aux {α : Type u_2} [Group α] {s : Finset α} :

(∃ (a : α), s = {a} ∧ IsUnit a) ↔ ∃ (a : α), s = {a}

@[simp]

theorem Finset.image_add_left {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} :

Finset.image (fun (b : α) => a + b) t = Finset.preimage t (fun (b : α) => -a + b) (_ : Set.InjOn (fun (x : α) => -a + x) ((fun (b : α) => -a + b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_mul_left {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} :

Finset.image (fun (b : α) => a * b) t = Finset.preimage t (fun (b : α) => a⁻¹ * b) (_ : Set.InjOn (fun (x : α) => a⁻¹ * x) ((fun (b : α) => a⁻¹ * b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_add_right {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} :

Finset.image (fun (x : α) => x + b) t = Finset.preimage t (fun (x : α) => x + -b) (_ : Set.InjOn (fun (x : α) => x + -b) ((fun (x : α) => x + -b) ⁻¹' ↑t))

@[simp]

theorem Finset.image_mul_right {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} :

Finset.image (fun (x : α) => x * b) t = Finset.preimage t (fun (x : α) => x * b⁻¹) (_ : Set.InjOn (fun (x : α) => x * b⁻¹) ((fun (x : α) => x * b⁻¹) ⁻¹' ↑t))

theorem Finset.image_add_left' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} :

Finset.image (fun (b : α) => -a + b) t = Finset.preimage t (fun (b : α) => a + b) (_ : Set.InjOn (fun (x : α) => a + x) ((fun (b : α) => a + b) ⁻¹' ↑t))

theorem Finset.image_mul_left' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} :

Finset.image (fun (b : α) => a⁻¹ * b) t = Finset.preimage t (fun (b : α) => a * b) (_ : Set.InjOn (fun (x : α) => a * x) ((fun (b : α) => a * b) ⁻¹' ↑t))

theorem Finset.image_add_right' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} :

Finset.image (fun (x : α) => x + -b) t = Finset.preimage t (fun (x : α) => x + b) (_ : Set.InjOn (fun (x : α) => x + b) ((fun (x : α) => x + b) ⁻¹' ↑t))

theorem Finset.image_mul_right' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} :

Finset.image (fun (x : α) => x * b⁻¹) t = Finset.preimage t (fun (x : α) => x * b) (_ : Set.InjOn (fun (x : α) => x * b) ((fun (x : α) => x * b) ⁻¹' ↑t))

theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [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 : α} :

Finset.preimage {b} (fun (x : α) => a + x) (_ : Set.InjOn (fun (x : α) => a + x) ((fun (x : α) => a + x) ⁻¹' ↑{b})) = {-a + b}

@[simp]

theorem Finset.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} :

Finset.preimage {b} (fun (x : α) => a * x) (_ : Set.InjOn (fun (x : α) => a * x) ((fun (x : α) => a * x) ⁻¹' ↑{b})) = {a⁻¹ * b}

@[simp]

theorem Finset.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} :

Finset.preimage {b} (fun (x : α) => x + a) (_ : Set.InjOn (fun (x : α) => x + a) ((fun (x : α) => x + a) ⁻¹' ↑{b})) = {b + -a}

@[simp]

theorem Finset.preimage_mul_right_singleton {α : Type u_2} [Group α] {a : α} {b : α} :

Finset.preimage {b} (fun (x : α) => x * a) (_ : Set.InjOn (fun (x : α) => x * a) ((fun (x : α) => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}

@[simp]

theorem Finset.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} :

Finset.preimage 0 (fun (x : α) => a + x) (_ : Set.InjOn (fun (x : α) => a + x) ((fun (x : α) => a + x) ⁻¹' ↑0)) = {-a}

@[simp]

theorem Finset.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} :

Finset.preimage 1 (fun (x : α) => a * x) (_ : Set.InjOn (fun (x : α) => a * x) ((fun (x : α) => a * x) ⁻¹' ↑1)) = {a⁻¹}

@[simp]

theorem Finset.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} :

Finset.preimage 0 (fun (x : α) => x + b) (_ : Set.InjOn (fun (x : α) => x + b) ((fun (x : α) => x + b) ⁻¹' ↑0)) = {-b}

@[simp]

theorem Finset.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} :

Finset.preimage 1 (fun (x : α) => x * b) (_ : Set.InjOn (fun (x : α) => x * b) ((fun (x : α) => x * b) ⁻¹' ↑1)) = {b⁻¹}

theorem Finset.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} :

Finset.preimage 0 (fun (x : α) => -a + x) (_ : Set.InjOn (fun (x : α) => -a + x) ((fun (x : α) => -a + x) ⁻¹' ↑0)) = {a}

theorem Finset.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} :

Finset.preimage 1 (fun (x : α) => a⁻¹ * x) (_ : Set.InjOn (fun (x : α) => a⁻¹ * x) ((fun (x : α) => a⁻¹ * x) ⁻¹' ↑1)) = {a}

theorem Finset.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} :

Finset.preimage 0 (fun (x : α) => x + -b) (_ : Set.InjOn (fun (x : α) => x + -b) ((fun (x : α) => x + -b) ⁻¹' ↑0)) = {b}

theorem Finset.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} :

Finset.preimage 1 (fun (x : α) => x * b⁻¹) (_ : Set.InjOn (fun (x : α) => x * b⁻¹) ((fun (x : α) => x * b⁻¹) ⁻¹' ↑1)) = {b}

Scalar addition/multiplication of finsets #

def Finset.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] :

VAdd (Finset α) (Finset β)

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

Equations

Finset.vadd = { vadd := Finset.image₂ fun (x : α) (x_1 : β) => x +ᵥ x_1 }

Instances For

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 (x : α) (x_1 : β) => x • x_1 }

Instances For

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 (x x_1 : β) => x -ᵥ x_1 }

Instances For

theorem Finset.vsub_def {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :

s -ᵥ t = Finset.image₂ (fun (x x_1 : β) => x -ᵥ x_1) s t

@[simp]

theorem Finset.image_vsub_product {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :

Finset.image₂ (fun (x x_1 : β) => x -ᵥ x_1) s t = s -ᵥ t

theorem Finset.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} {a : α} :

a ∈ s -ᵥ t ↔ ∃ b ∈ 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 }

Instances For

def Finset.smulFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] :

SMul α (Finset β)

The scaling of a finset s by a scalar a: a • s = {a • x | x ∈ s}.

Equations

Finset.smulFinset = { smul := fun (a : α) => Finset.image fun (x : β) => a • x }

Instances For

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_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 β) :

(Finset.biUnion s fun (x : α) => x +ᵥ t) = s +ᵥ t

@[simp]

theorem Finset.biUnion_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) :

(Finset.biUnion s 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

(_ : VAddCommClass α β (Finset γ)) = (_ : VAddCommClass α β (Finset γ))

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

SMulCommClass α β (Finset γ)

Equations

(_ : SMulCommClass α β (Finset γ)) = (_ : SMulCommClass α β (Finset γ))

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

VAddCommClass α (Finset β) (Finset γ)

Equations

(_ : VAddCommClass α (Finset β) (Finset γ)) = (_ : VAddCommClass α (Finset β) (Finset γ))

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

SMulCommClass α (Finset β) (Finset γ)

Equations

(_ : SMulCommClass α (Finset β) (Finset γ)) = (_ : SMulCommClass α (Finset β) (Finset γ))

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

VAddCommClass (Finset α) β (Finset γ)

Equations

(_ : VAddCommClass (Finset α) β (Finset γ)) = (_ : VAddCommClass (Finset α) β (Finset γ))

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

SMulCommClass (Finset α) β (Finset γ)

Equations

(_ : SMulCommClass (Finset α) β (Finset γ)) = (_ : SMulCommClass (Finset α) β (Finset γ))

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

VAddCommClass (Finset α) (Finset β) (Finset γ)

Equations

(_ : VAddCommClass (Finset α) (Finset β) (Finset γ)) = (_ : VAddCommClass (Finset α) (Finset β) (Finset γ))

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

SMulCommClass (Finset α) (Finset β) (Finset γ)

Equations

(_ : SMulCommClass (Finset α) (Finset β) (Finset γ)) = (_ : SMulCommClass (Finset α) (Finset β) (Finset γ))

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

VAddAssocClass α β (Finset γ)

Equations

(_ : VAddAssocClass α β (Finset γ)) = (_ : VAddAssocClass α β (Finset γ))

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

IsScalarTower α β (Finset γ)

Equations

(_ : IsScalarTower α β (Finset γ)) = (_ : IsScalarTower α β (Finset γ))

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

VAddAssocClass α (Finset β) (Finset γ)

Equations

(_ : VAddAssocClass α (Finset β) (Finset γ)) = (_ : VAddAssocClass α (Finset β) (Finset γ))

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

IsScalarTower α (Finset β) (Finset γ)

Equations

(_ : IsScalarTower α (Finset β) (Finset γ)) = (_ : IsScalarTower α (Finset β) (Finset γ))

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

VAddAssocClass (Finset α) (Finset β) (Finset γ)

Equations

(_ : VAddAssocClass (Finset α) (Finset β) (Finset γ)) = (_ : VAddAssocClass (Finset α) (Finset β) (Finset γ))

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

IsScalarTower (Finset α) (Finset β) (Finset γ)

Equations

(_ : IsScalarTower (Finset α) (Finset β) (Finset γ)) = (_ : IsScalarTower (Finset α) (Finset β) (Finset γ))

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

IsCentralVAdd α (Finset β)

Equations

(_ : IsCentralVAdd α (Finset β)) = (_ : IsCentralVAdd α (Finset β))

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

IsCentralScalar α (Finset β)

Equations

(_ : IsCentralScalar α (Finset β)) = (_ : IsCentralScalar α (Finset β))

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 (x : α) (x_3 : β) => x +ᵥ x_3) (Finset.image₂ (fun (x x_3 : α) => x + x_3) x x_1) x_2 = Finset.image₂ (fun (x : α) (x_3 : β) => x +ᵥ x_3) x (Finset.image₂ (fun (x : α) (x_3 : β) => x +ᵥ x_3) x_1 x_2)

theorem Finset.addAction.proof_1 {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddMonoid α] [AddAction α β] (s : Finset β) :

Finset.image₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) {0} s = s

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

One or more equations did not get rendered due to their size.

Instances For

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

One or more equations did not get rendered due to their size.

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a +ᵥ s) = a +ᵥ ↑s)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

Instances For

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

One or more equations did not get rendered due to their size.

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

Instances For

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 (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

Instances For

instance Finset.instNoZeroDivisorsFinsetMulZero {α : Type u_2} [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] :

NoZeroDivisors (Finset α)

Equations

(_ : NoZeroDivisors (Finset α)) = (_ : NoZeroDivisors (Finset α))

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

NoZeroSMulDivisors (Finset α) (Finset β)

Equations

(_ : NoZeroSMulDivisors (Finset α) (Finset β)) = (_ : NoZeroSMulDivisors (Finset α) (Finset β))

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

NoZeroSMulDivisors α (Finset β)

Equations

(_ : NoZeroSMulDivisors α (Finset β)) = (_ : NoZeroSMulDivisors α (Finset β))

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 α) :

(Finset.biUnion t fun (a : α) => AddOpposite.op a +ᵥ s) = s + t

@[simp]

theorem Finset.biUnion_op_smul_finset {α : Type u_2} [Mul α] [DecidableEq α] (s : Finset α) (t : Finset α) :

(Finset.biUnion t 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 α} :

(Set.PairwiseDisjoint s 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 α} :

(Set.PairwiseDisjoint s 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

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

theorem Finset.card_dvd_card_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {t : Finset β} {s : Finset α} :

Set.PairwiseDisjoint ((fun (x : α) => x +ᵥ t) '' ↑s) 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 α} :

Set.PairwiseDisjoint ((fun (x : α) => x • t) '' ↑s) 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 α} :

Set.PairwiseDisjoint ((fun (b : α) => Finset.image (fun (a : α) => a + b) s) '' ↑t) 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 α} :

Set.PairwiseDisjoint ((fun (b : α) => Finset.image (fun (a : α) => a * b) s) '' ↑t) 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 α} :

Set.PairwiseDisjoint ((fun (x : α) => x +ᵥ t) '' ↑s) 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 α} :

Set.PairwiseDisjoint ((fun (x : α) => x • t) '' ↑s) 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 : Finset.Nontrivial s) :

s • Finset.univ = Finset.univ

@[simp]

theorem Finset.inv_zero {α : Type u_2} [GroupWithZero α] [DecidableEq α] :

@[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 : ι → α) :

(Finset.sum (-s) fun (i : ι) => f i) = Finset.sum s fun (i : ι) => f (-i)

@[simp]

theorem Finset.prod_inv_index {α : Type u_2} [CommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) :

(Finset.prod s⁻¹ fun (i : ι) => f i) = Finset.prod s fun (i : ι) => f i⁻¹

@[simp]

theorem Finset.prod_neg_index {α : Type u_2} [CommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) :

(Finset.prod (-s) fun (i : ι) => f i) = Finset.prod s fun (i : ι) => f (-i)

@[simp]

theorem Finset.sum_inv_index {α : Type u_2} [AddCommMonoid α] {ι : Type u_5} [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) :

(Finset.sum s⁻¹ fun (i : ι) => f i) = Finset.sum s fun (i : ι) => f i⁻¹

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)⁻¹

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

@[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 0)) :

Set.Finite.toFinset h = 0

@[simp]

theorem Set.Finite.toFinset_one {α : Type u_2} [One α] (h : optParam (Set.Finite 1) (_ : 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)] :

Set.toFinset (s + t) = Set.toFinset s + Set.toFinset t

@[simp]

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

Set.toFinset (s * t) = Set.toFinset s * Set.toFinset t

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

Set.Finite.toFinset hf = Set.Finite.toFinset hs + Set.Finite.toFinset ht

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

Set.Finite.toFinset hf = Set.Finite.toFinset hs * Set.Finite.toFinset ht

@[simp]

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

Set.toFinset (s +ᵥ t) = Set.toFinset s +ᵥ Set.toFinset t

@[simp]

theorem Set.toFinset_smul {α : Type u_2} {β : Type u_3} [SMul α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s • t)] :

Set.toFinset (s • t) = Set.toFinset s • Set.toFinset t

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

Set.Finite.toFinset hf = Set.Finite.toFinset hs +ᵥ Set.Finite.toFinset ht

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

Set.Finite.toFinset hf = Set.Finite.toFinset hs • Set.Finite.toFinset ht

@[simp]

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

Set.toFinset (a +ᵥ s) = a +ᵥ Set.toFinset s

@[simp]

theorem Set.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a • s)] :

Set.toFinset (a • s) = a • Set.toFinset s

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

Set.Finite.toFinset hf = a +ᵥ Set.Finite.toFinset hs

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

Set.Finite.toFinset hf = a • Set.Finite.toFinset hs

@[simp]

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

Set.toFinset (s -ᵥ t) = Set.toFinset s -ᵥ Set.toFinset t

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

Set.Finite.toFinset hf = Set.Finite.toFinset hs -ᵥ Set.Finite.toFinset ht

@[simp]

theorem Set.card_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (s : Set β) :

Nat.card ↑(a +ᵥ s) = Nat.card ↑s

@[simp]

theorem Set.card_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (s : Set β) :

Nat.card ↑(a • s) = Nat.card ↑s

theorem Set.card_add_le {α : Type u_2} [Add α] [IsCancelAdd α] {s : Set α} {t : Set α} :

Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t

theorem Set.card_mul_le {α : Type u_2} [Mul α] [IsCancelMul α] {s : Set α} {t : Set α} :

Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

@[simp]

theorem Set.card_neg {α : Type u_2} [InvolutiveNeg α] (s : Set α) :

Nat.card ↑(-s) = Nat.card ↑s

@[simp]

theorem Set.card_inv {α : Type u_2} [InvolutiveInv α] (s : Set α) :

Nat.card ↑s⁻¹ = Nat.card ↑s

theorem Set.card_sub_le {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :

Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t

theorem Set.card_div_le {α : Type u_2} [Group α] {s : Set α} {t : Set α} :

Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t

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

DecidablePred fun (x : ℕ) => x ∈ a +ᵥ s

Equations

Nat.decidablePred_mem_vadd_set a n = decidable_of_iff' (a ≤ n ∧ n - a ∈ s) (_ : (fun (x : ℕ) => x ∈ a +ᵥ s) n ↔ a ≤ n ∧ n - a ∈ s)