mathlib documentation

algebra.pointwise

Pointwise addition, multiplication, and scalar multiplication of sets.

This file defines pointwise algebraic operations on sets.

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

Implementation notes

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication

Properties about 1

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

Properties about multiplication

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

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

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

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

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

@[simp]
theorem set.preimage_add_left_singleton {α : Type u_1} {a b : α} [add_group α] :
has_add.add a ⁻¹' {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} [add_semigroup α] :

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

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

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

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

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

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

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

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

theorem set.singleton.is_add_hom {α : Type u_1} [has_add α] :

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

theorem set.add_subset_add {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_add α] :
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]
theorem set.univ_add_univ {α : Type u_1} [add_monoid α] :

@[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
def set.singleton_add_hom {α : Type u_1} [add_monoid α] :
α →+ 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] :

addition preserves finiteness

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

multiplication preserves finiteness

Equations

Properties about inversion

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

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

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

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

Properties about scalar multiplication

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

Scaling a set: multiplying every element by a scalar.

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

theorem set.mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {x : β} [has_scalar α β] {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 : β} [has_scalar α β] {t : set β} :
y ta y a t

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

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

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

@[instance]
def set.has_scalar {α : Type u_1} {β : Type u_2} [has_scalar α β] :
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 α} [has_scalar α β] {t : set β} :

theorem set.mem_smul {α : Type u_1} {β : Type u_2} {s : set α} {x : β} [has_scalar α β] {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 α} [has_scalar α β] {t : set β} :
(λ (x : α × β), x.fst x.snd) '' s.prod t = s t

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

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

set α as a (∪,*)-semiring

@[instance]

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

The identitiy function set α → set_semiring α.

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

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.mul_action_set {α : Type u_1} {β : Type u_2} [monoid α] [mul_action α β] :
mul_action α (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 α] [add_comm_monoid β] [semimodule α β] {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 α] [mul_action α β] {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 α] [mul_action α β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a A a⁻¹ x A

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

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