# mathlibdocumentation

algebra.pointwise

# Pointwise addition, multiplication, and scalar multiplication of sets.

This file defines pointwise algebraic operations on sets.

• For a type α with multiplication, multiplication is defined on set α by taking s * t to be the set of all x * y where x ∈ s and y ∈ t. Similarly for addition.
• For α a semigroup, set α is a semigroup.
• If α is a (commutative) monoid, we define an alias set_semiring α for set α, which then becomes a (commutative) semiring with union as addition and pointwise multiplication as multiplication.
• For a type β with scalar multiplication by another type α, this file defines a scalar multiplication of set β by set α and a separate scalar multiplication of set β by α.
• We also define pointwise multiplication on finset.

Appropriate definitions and results are also transported to the additive theory via to_additive.

## Implementation notes

• The following expressions are considered in simp-normal form in a group: (λ h, h * g) ⁻¹' s, (λ h, g * h) ⁻¹' s, (λ h, h * g⁻¹) ⁻¹' s, (λ h, g⁻¹ * h) ⁻¹' s, s * t, s⁻¹, (1 : set _) (and similarly for additive variants). Expressions equal to one of these will be simplified.

## Tags

@[instance]
def set.has_one {α : Type u_1} [has_one α] :

Equations
@[instance]
def set.has_zero {α : Type u_1} [has_zero α] :

theorem set.singleton_one {α : Type u_1} [has_one α] :
{1} = 1

theorem set.singleton_zero {α : Type u_1} [has_zero α] :
{0} = 0

@[simp]
theorem set.mem_one {α : Type u_1} {a : α} [has_one α] :
a 1 a = 1

@[simp]
theorem set.mem_zero {α : Type u_1} {a : α} [has_zero α] :
a 0 a = 0

theorem set.zero_mem_zero {α : Type u_1} [has_zero α] :
0 0

theorem set.one_mem_one {α : Type u_1} [has_one α] :
1 1

@[simp]
theorem set.zero_subset {α : Type u_1} {s : set α} [has_zero α] :
0 s 0 s

@[simp]
theorem set.one_subset {α : Type u_1} {s : set α} [has_one α] :
1 s 1 s

theorem set.zero_nonempty {α : Type u_1} [has_zero α] :

theorem set.one_nonempty {α : Type u_1} [has_one α] :

@[simp]
theorem set.image_zero {α : Type u_1} {β : Type u_2} [has_zero α] {f : α → β} :
f '' 0 = {f 0}

@[simp]
theorem set.image_one {α : Type u_1} {β : Type u_2} [has_one α] {f : α → β} :
f '' 1 = {f 1}

@[instance]
def set.has_mul {α : Type u_1} [has_mul α] :

Equations
@[instance]

@[simp]
theorem set.image2_mul {α : Type u_1} {s t : set α} [has_mul α] :
= s * t

@[simp]
theorem set.image2_add {α : Type u_1} {s t : set α} [has_add α] :
= s + t

theorem set.mem_add {α : Type u_1} {s t : set α} {a : α} [has_add α] :
a s + t ∃ (x y : α), x s y t x + y = a

theorem set.mem_mul {α : Type u_1} {s t : set α} {a : α} [has_mul α] :
a s * t ∃ (x y : α), x s y t x * y = a

theorem set.mul_mem_mul {α : Type u_1} {s t : set α} {a b : α} [has_mul α] :
a sb ta * b s * t

theorem set.add_mem_add {α : Type u_1} {s t : set α} {a b : α} [has_add α] :
a sb ta + b s + t

theorem set.image_mul_prod {α : Type u_1} {s t : set α} [has_mul α] :
(λ (x : α × α), (x.fst) * x.snd) '' s.prod t = s * t

theorem set.add_image_prod {α : Type u_1} {s t : set α} [has_add α] :
(λ (x : α × α), x.fst + x.snd) '' s.prod t = s + t

@[simp]
theorem set.image_add_left {α : Type u_1} {t : set α} {a : α} [add_group α] :
(λ (b : α), a + b) '' t = (λ (b : α), -a + b) ⁻¹' t

@[simp]
theorem set.image_mul_left {α : Type u_1} {t : set α} {a : α} [group α] :
(λ (b : α), a * b) '' t = (λ (b : α), a⁻¹ * b) ⁻¹' t

@[simp]
theorem set.image_mul_right {α : Type u_1} {t : set α} {b : α} [group α] :
(λ (a : α), a * b) '' t = (λ (a : α), a * b⁻¹) ⁻¹' t

@[simp]
theorem set.image_add_right {α : Type u_1} {t : set α} {b : α} [add_group α] :
(λ (a : α), a + b) '' t = (λ (a : α), a + -b) ⁻¹' t

theorem set.image_mul_left' {α : Type u_1} {t : set α} {a : α} [group α] :
(λ (b : α), a⁻¹ * b) '' t = (λ (b : α), a * b) ⁻¹' t

theorem set.image_add_left' {α : Type u_1} {t : set α} {a : α} [add_group α] :
(λ (b : α), -a + b) '' t = (λ (b : α), a + b) ⁻¹' t

theorem set.image_mul_right' {α : Type u_1} {t : set α} {b : α} [group α] :
(λ (a : α), a * b⁻¹) '' t = (λ (a : α), a * b) ⁻¹' t

theorem set.image_add_right' {α : Type u_1} {t : set α} {b : α} [add_group α] :
(λ (a : α), a + -b) '' t = (λ (a : α), a + b) ⁻¹' t

@[simp]
theorem set.preimage_mul_left_singleton {α : Type u_1} {a b : α} [group α] :
⁻¹' {b} = {a⁻¹ * b}

@[simp]
theorem set.preimage_add_left_singleton {α : Type u_1} {a b : α} [add_group α] :
⁻¹' {b} = {-a + b}

@[simp]
theorem set.preimage_mul_right_singleton {α : Type u_1} {a b : α} [group α] :
(λ (_x : α), _x * a) ⁻¹' {b} = {b * a⁻¹}

@[simp]
theorem set.preimage_add_right_singleton {α : Type u_1} {a b : α} [add_group α] :
(λ (_x : α), _x + a) ⁻¹' {b} = {b + -a}

@[simp]
theorem set.preimage_mul_left_one {α : Type u_1} {a : α} [group α] :
(λ (b : α), a * b) ⁻¹' 1 = {a⁻¹}

@[simp]
theorem set.preimage_add_left_zero {α : Type u_1} {a : α} [add_group α] :
(λ (b : α), a + b) ⁻¹' 0 = {-a}

@[simp]
theorem set.preimage_add_right_zero {α : Type u_1} {b : α} [add_group α] :
(λ (a : α), a + b) ⁻¹' 0 = {-b}

@[simp]
theorem set.preimage_mul_right_one {α : Type u_1} {b : α} [group α] :
(λ (a : α), a * b) ⁻¹' 1 = {b⁻¹}

theorem set.preimage_add_left_zero' {α : Type u_1} {a : α} [add_group α] :
(λ (b : α), -a + b) ⁻¹' 0 = {a}

theorem set.preimage_mul_left_one' {α : Type u_1} {a : α} [group α] :
(λ (b : α), a⁻¹ * b) ⁻¹' 1 = {a}

theorem set.preimage_add_right_zero' {α : Type u_1} {b : α} [add_group α] :
(λ (a : α), a + -b) ⁻¹' 0 = {b}

theorem set.preimage_mul_right_one' {α : Type u_1} {b : α} [group α] :
(λ (a : α), a * b⁻¹) ⁻¹' 1 = {b}

@[simp]
theorem set.add_singleton {α : Type u_1} {s : set α} {b : α} [has_add α] :
s + {b} = (λ (a : α), a + b) '' s

@[simp]
theorem set.mul_singleton {α : Type u_1} {s : set α} {b : α} [has_mul α] :
s * {b} = (λ (a : α), a * b) '' s

@[simp]
theorem set.singleton_add {α : Type u_1} {t : set α} {a : α} [has_add α] :
{a} + t = (λ (b : α), a + b) '' t

@[simp]
theorem set.singleton_mul {α : Type u_1} {t : set α} {a : α} [has_mul α] :
{a} * t = (λ (b : α), a * b) '' t

@[simp]
theorem set.singleton_mul_singleton {α : Type u_1} {a b : α} [has_mul α] :
{a} * {b} = {a * b}

@[simp]
theorem set.singleton_add_singleton {α : Type u_1} {a b : α} [has_add α] :
{a} + {b} = {a + b}

@[instance]
def set.add_semigroup {α : Type u_1}  :

@[instance]
def set.semigroup {α : Type u_1} [semigroup α] :

Equations
@[instance]
def set.monoid {α : Type u_1} [monoid α] :
monoid (set α)

Equations
@[instance]

theorem set.mul_comm {α : Type u_1} {s t : set α}  :
s * t = t * s

theorem set.add_comm {α : Type u_1} {s t : set α}  :
s + t = t + s

@[instance]
def set.comm_monoid {α : Type u_1} [comm_monoid α] :

Equations
@[instance]
def set.add_comm_monoid {α : Type u_1}  :

theorem set.singleton.is_mul_hom {α : Type u_1} [has_mul α] :

@[simp]
theorem set.empty_mul {α : Type u_1} {s : set α} [has_mul α] :

@[simp]
theorem set.empty_add {α : Type u_1} {s : set α} [has_add α] :

@[simp]
theorem set.add_empty {α : Type u_1} {s : set α} [has_add α] :

@[simp]
theorem set.mul_empty {α : Type u_1} {s : set α} [has_mul α] :

s₁ t₁s₂ t₂s₁ + s₂ t₁ + t₂

theorem set.mul_subset_mul {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_mul α] :
s₁ t₁s₂ t₂s₁ * s₂ t₁ * t₂

theorem set.union_mul {α : Type u_1} {s t u : set α} [has_mul α] :
(s t) * u = s * u t * u

theorem set.union_add {α : Type u_1} {s t u : set α} [has_add α] :
s t + u = s + u (t + u)

theorem set.mul_union {α : Type u_1} {s t u : set α} [has_mul α] :
s * (t u) = s * t s * u

theorem set.add_union {α : Type u_1} {s t u : set α} [has_add α] :
s + (t u) = s + t (s + u)

theorem set.Union_mul_left_image {α : Type u_1} {s t : set α} [has_mul α] :
(⋃ (a : α) (H : a s), (λ (x : α), a * x) '' t) = s * t

theorem set.Union_add_left_image {α : Type u_1} {s t : set α} [has_add α] :
(⋃ (a : α) (H : a s), (λ (x : α), a + x) '' t) = s + t

theorem set.Union_mul_right_image {α : Type u_1} {s t : set α} [has_mul α] :
(⋃ (a : α) (H : a t), (λ (x : α), x * a) '' s) = s * t

theorem set.Union_add_right_image {α : Type u_1} {s t : set α} [has_add α] :
(⋃ (a : α) (H : a t), (λ (x : α), x + a) '' s) = s + t

@[simp]

@[simp]
theorem set.univ_mul_univ {α : Type u_1} [monoid α] :

def set.singleton_hom {α : Type u_1} [monoid α] :
α →* set α

singleton is a monoid hom.

Equations
α →+ set α

singleton is an add monoid hom

theorem set.nonempty.add {α : Type u_1} {s t : set α} [has_add α] :
s.nonemptyt.nonempty(s + t).nonempty

theorem set.nonempty.mul {α : Type u_1} {s t : set α} [has_mul α] :
s.nonemptyt.nonempty(s * t).nonempty

theorem set.finite.mul {α : Type u_1} {s t : set α} [has_mul α] :
s.finitet.finite(s * t).finite

theorem set.finite.add {α : Type u_1} {s t : set α} [has_add α] :
s.finitet.finite(s + t).finite

def set.fintype_add {α : Type u_1} [has_add α] [decidable_eq α] (s t : set α) [hs : fintype s] [ht : fintype t] :

def set.fintype_mul {α : Type u_1} [has_mul α] [decidable_eq α] (s t : set α) [hs : fintype s] [ht : fintype t] :

multiplication preserves finiteness

Equations

@[instance]
def set.has_neg' {α : Type u_1} [has_neg α] :

@[instance]
def set.has_inv {α : Type u_1} [has_inv α] :

Equations
@[simp]
theorem set.mem_inv {α : Type u_1} {s : set α} {a : α} [has_inv α] :

@[simp]
theorem set.mem_neg {α : Type u_1} {s : set α} {a : α} [has_neg α] :
a -s -a s

theorem set.inv_mem_inv {α : Type u_1} {s : set α} {a : α} [group α] :

theorem set.neg_mem_neg {α : Type u_1} {s : set α} {a : α} [add_group α] :
-a -s a s

@[simp]
theorem set.inv_preimage {α : Type u_1} {s : set α} [has_inv α] :

@[simp]
theorem set.neg_preimage {α : Type u_1} {s : set α} [has_neg α] :
= -s

@[simp]
theorem set.image_inv {α : Type u_1} {s : set α} [group α] :

@[simp]
theorem set.image_neg {α : Type u_1} {s : set α} [add_group α] :
= -s

@[simp]
theorem set.inter_neg {α : Type u_1} {s t : set α} [has_neg α] :
-(s t) = -s -t

@[simp]
theorem set.inter_inv {α : Type u_1} {s t : set α} [has_inv α] :

@[simp]
theorem set.union_neg {α : Type u_1} {s t : set α} [has_neg α] :
-(s t) = -s -t

@[simp]
theorem set.union_inv {α : Type u_1} {s t : set α} [has_inv α] :

@[simp]
theorem set.compl_neg {α : Type u_1} {s : set α} [has_neg α] :
-s = (-s)

@[simp]
theorem set.compl_inv {α : Type u_1} {s : set α} [has_inv α] :

@[simp]
theorem set.neg_neg {α : Type u_1} {s : set α} [add_group α] :
--s = s

@[simp]
theorem set.inv_inv {α : Type u_1} {s : set α} [group α] :

@[simp]
theorem set.univ_neg {α : Type u_1} [add_group α] :

@[simp]
theorem set.univ_inv {α : Type u_1} [group α] :

@[simp]
theorem set.neg_subset_neg {α : Type u_1} [add_group α] {s t : set α} :
-s -t s t

@[simp]
theorem set.inv_subset_inv {α : Type u_1} [group α] {s t : set α} :

theorem set.inv_subset {α : Type u_1} [group α] {s t : set α} :

theorem set.neg_subset {α : Type u_1} [add_group α] {s t : set α} :
-s t s -t

@[instance]
def set.has_scalar_set {α : Type u_1} {β : Type u_2} [ β] :
(set β)

Scaling a set: multiplying every element by a scalar.

Equations
@[simp]
theorem set.image_smul {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
(λ (x : β), a x) '' t = a t

theorem set.mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {x : β} [ β] {t : set β} :
x a t ∃ (y : β), y t a y = x

theorem set.smul_mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {y : β} [ β] {t : set β} :
y ta y a t

theorem set.smul_set_union {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
a (s t) = a s a t

@[simp]
theorem set.smul_set_empty {α : Type u_1} {β : Type u_2} [ β] (a : α) :

theorem set.smul_set_mono {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
s ta s a t

@[instance]
def set.has_scalar {α : Type u_1} {β : Type u_2} [ β] :
has_scalar (set α) (set β)

Pointwise scalar multiplication by a set of scalars.

Equations
@[simp]
theorem set.image2_smul {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
= s t

theorem set.mem_smul {α : Type u_1} {β : Type u_2} {s : set α} {x : β} [ β] {t : set β} :
x s t ∃ (a : α) (y : β), a s y t a y = x

theorem set.image_smul_prod {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
(λ (x : α × β), x.fst x.snd) '' s.prod t = s t

theorem set.range_smul_range {α : Type u_1} {β : Type u_2} [ β] {ι : Type u_3} {κ : Type u_4} (b : ι → α) (c : κ → β) :
= set.range (λ (p : ι × κ), b p.fst c p.snd)

theorem set.singleton_smul {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
{a} t = a t

### set α as a (∪,*)-semiring

@[instance]
def set.set_semiring.inhabited (α : Type u_1) :

def set.set_semiring  :
Type u_1Type u_1

An alias for set α, which has a semiring structure given by ∪ as "addition" and pointwise multiplication * as "multiplication".

Equations
def set.up {α : Type u_1} :
set α

The identitiy function set α → set_semiring α.

Equations
def set.set_semiring.down {α : Type u_1} :
set α

The identitiy function set_semiring α → set α.

Equations
@[simp]
theorem set.down_up {α : Type u_1} {s : set α} :
s.up.down = s

@[simp]
theorem set.up_down {α : Type u_1} {s : set.set_semiring α} :
s.down.up = s

@[instance]
def set.set_semiring.semiring {α : Type u_1} [monoid α] :

Equations
@[instance]
def set.set_semiring.comm_semiring {α : Type u_1} [comm_monoid α] :

Equations
@[instance]
def set.mul_action_set {α : Type u_1} {β : Type u_2} [monoid α] [ β] :
(set β)

A multiplicative action of a monoid on a type β gives also a multiplicative action on the subsets of β.

Equations
theorem set.image_add {α : Type u_1} {β : Type u_2} {s t : set α} [has_add α] [has_add β] (m : α → β) [is_add_hom m] :
m '' (s + t) = m '' s + m '' t

theorem set.image_mul {α : Type u_1} {β : Type u_2} {s t : set α} [has_mul α] [has_mul β] (m : α → β) [is_mul_hom m] :
m '' s * t = (m '' s) * m '' t

theorem set.preimage_mul_preimage_subset {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (m : α → β) [is_mul_hom m] {s t : set β} :
(m ⁻¹' s) * m ⁻¹' t m ⁻¹' s * t

theorem set.preimage_add_preimage_subset {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (m : α → β) [is_add_hom m] {s t : set β} :
m ⁻¹' s + m ⁻¹' t m ⁻¹' (s + t)

def set.image_hom {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] :
→* β)

The image of a set under function is a ring homomorphism with respect to the pointwise operations on sets.

Equations
theorem zero_smul_set {α : Type u_1} {β : Type u_2} [semiring α] [ β] {s : set β} :
s.nonempty0 s = 0

A nonempty set in a semimodule is scaled by zero to the singleton containing 0 in the semimodule.

theorem mem_inv_smul_set_iff {α : Type u_1} {β : Type u_2} [field α] [ β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a⁻¹ A a x A

theorem mem_smul_set_iff_inv_smul_mem {α : Type u_1} {β : Type u_2} [field α] [ β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a A a⁻¹ x A

@[instance]

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

@[instance]
def finset.has_mul {α : Type u_1} [decidable_eq α] [has_mul α] :

The pointwise product of two finite sets s and t: st = s ⬝ t = s * t = { x * y | x ∈ s, y ∈ t }.

Equations
theorem finset.add_def {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
s + t = finset.image (λ (p : α × α), p.fst + p.snd) (s.product t)

theorem finset.mul_def {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = finset.image (λ (p : α × α), (p.fst) * p.snd) (s.product t)

theorem finset.mem_mul {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} {x : α} :
x s * t ∃ (y z : α), y s z t y * z = x

theorem finset.mem_add {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} {x : α} :
x s + t ∃ (y z : α), y s z t y + z = x

@[simp]
theorem finset.coe_add {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t) = s + t

@[simp]
theorem finset.coe_mul {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = (s) * t

theorem finset.mul_mem_mul {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} {x y : α} :
x sy tx * y s * t

theorem finset.add_mem_add {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} {x y : α} :
x sy tx + y s + t

theorem finset.add_card_le {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card (s.card) * t.card

theorem finset.mul_card_le {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card (s.card) * t.card