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 #

set multiplication, set addition, pointwise addition, pointwise multiplication

Properties about 1 #

source

@[protected, instance]

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

has_one (set α)

Equations

set.has_one = {one := {1}}

source

@[protected, instance]

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

has_zero (set α)

source

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

{1} = 1

source

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

{0} = 0

source

@[simp]

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

a ∈ 1 ↔ a = 1

source

@[simp]

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

a ∈ 0 ↔ a = 0

source

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

0 ∈ 0

source

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

1 ∈ 1

source

@[simp]

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

0 ⊆ s ↔ 0 ∈ s

source

@[simp]

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

1 ⊆ s ↔ 1 ∈ s

source

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

0.nonempty

source

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

1.nonempty

source

@[simp]

theorem set.image_zero {α : Type u_1} {β : Type u_2} [has_zero α] {f : α → β} :

f '' 0 = {f 0}

source

@[simp]

theorem set.image_one {α : Type u_1} {β : Type u_2} [has_one α] {f : α → β} :

f '' 1 = {f 1}

Properties about multiplication #

source

@[protected, instance]

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

has_mul (set α)

Equations

set.has_mul = {mul := set.image2 has_mul.mul}

source

@[protected, instance]

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

has_add (set α)

source

@[simp]

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

set.image2 has_mul.mul s t = s * t

source

@[simp]

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

set.image2 has_add.add s t = s + t

source

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

source

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

source

theorem set.mul_mem_mul {α : Type u_1} {s t : set α} {a b : α} [has_mul α] (ha : a ∈ s) (hb : b ∈ t) :

a * b ∈ s * t

source

theorem set.add_mem_add {α : Type u_1} {s t : set α} {a b : α} [has_add α] (ha : a ∈ s) (hb : b ∈ t) :

a + b ∈ s + t

source

theorem set.image_mul_prod {α : Type u_1} {s t : set α} [has_mul α] :

(λ (x : α × α), (x.fst) * x.snd) '' s.prod t = s * t

source

theorem set.add_image_prod {α : Type u_1} {s t : set α} [has_add α] :

(λ (x : α × α), x.fst + x.snd) '' s.prod t = s + t

source

@[simp]

theorem set.image_add_left {α : Type u_1} {t : set α} {a : α} [add_group α] :

(λ (b : α), a + b) '' t = (λ (b : α), -a + b) ⁻¹' t

source

@[simp]

theorem set.image_mul_left {α : Type u_1} {t : set α} {a : α} [group α] :

(λ (b : α), a * b) '' t = (λ (b : α), a⁻¹ * b) ⁻¹' t

source

@[simp]

theorem set.image_mul_right {α : Type u_1} {t : set α} {b : α} [group α] :

(λ (a : α), a * b) '' t = (λ (a : α), a * b⁻¹) ⁻¹' t

source

@[simp]

theorem set.image_add_right {α : Type u_1} {t : set α} {b : α} [add_group α] :

(λ (a : α), a + b) '' t = (λ (a : α), a + -b) ⁻¹' t

source

theorem set.image_mul_left' {α : Type u_1} {t : set α} {a : α} [group α] :

(λ (b : α), a⁻¹ * b) '' t = (λ (b : α), a * b) ⁻¹' t

source

theorem set.image_add_left' {α : Type u_1} {t : set α} {a : α} [add_group α] :

(λ (b : α), -a + b) '' t = (λ (b : α), a + b) ⁻¹' t

source

theorem set.image_mul_right' {α : Type u_1} {t : set α} {b : α} [group α] :

(λ (a : α), a * b⁻¹) '' t = (λ (a : α), a * b) ⁻¹' t

source

theorem set.image_add_right' {α : Type u_1} {t : set α} {b : α} [add_group α] :

(λ (a : α), a + -b) '' t = (λ (a : α), a + b) ⁻¹' t

source

@[simp]

theorem set.preimage_mul_left_singleton {α : Type u_1} {a b : α} [group α] :

has_mul.mul a ⁻¹' {b} = {a⁻¹ * b}

source

@[simp]

theorem set.preimage_add_left_singleton {α : Type u_1} {a b : α} [add_group α] :

has_add.add a ⁻¹' {b} = {-a + b}

source

@[simp]

theorem set.preimage_mul_right_singleton {α : Type u_1} {a b : α} [group α] :

(λ (_x : α), _x * a) ⁻¹' {b} = {b * a⁻¹}

source

@[simp]

theorem set.preimage_add_right_singleton {α : Type u_1} {a b : α} [add_group α] :

(λ (_x : α), _x + a) ⁻¹' {b} = {b + -a}

source

@[simp]

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

(λ (b : α), a * b) ⁻¹' 1 = {a⁻¹}

source

@[simp]

theorem set.preimage_add_left_zero {α : Type u_1} {a : α} [add_group α] :

(λ (b : α), a + b) ⁻¹' 0 = {-a}

source

@[simp]

theorem set.preimage_add_right_zero {α : Type u_1} {b : α} [add_group α] :

(λ (a : α), a + b) ⁻¹' 0 = {-b}

source

@[simp]

theorem set.preimage_mul_right_one {α : Type u_1} {b : α} [group α] :

(λ (a : α), a * b) ⁻¹' 1 = {b⁻¹}

source

theorem set.preimage_add_left_zero' {α : Type u_1} {a : α} [add_group α] :

(λ (b : α), -a + b) ⁻¹' 0 = {a}

source

theorem set.preimage_mul_left_one' {α : Type u_1} {a : α} [group α] :

(λ (b : α), a⁻¹ * b) ⁻¹' 1 = {a}

source

theorem set.preimage_add_right_zero' {α : Type u_1} {b : α} [add_group α] :

(λ (a : α), a + -b) ⁻¹' 0 = {b}

source

theorem set.preimage_mul_right_one' {α : Type u_1} {b : α} [group α] :

(λ (a : α), a * b⁻¹) ⁻¹' 1 = {b}

source

@[simp]

theorem set.add_singleton {α : Type u_1} {s : set α} {b : α} [has_add α] :

s + {b} = (λ (a : α), a + b) '' s

source

@[simp]

theorem set.mul_singleton {α : Type u_1} {s : set α} {b : α} [has_mul α] :

s * {b} = (λ (a : α), a * b) '' s

source

@[simp]

theorem set.singleton_add {α : Type u_1} {t : set α} {a : α} [has_add α] :

{a} + t = (λ (b : α), a + b) '' t

source

@[simp]

theorem set.singleton_mul {α : Type u_1} {t : set α} {a : α} [has_mul α] :

{a} * t = (λ (b : α), a * b) '' t

source

@[simp]

theorem set.singleton_mul_singleton {α : Type u_1} {a b : α} [has_mul α] :

{a} * {b} = {a * b}

source

@[simp]

theorem set.singleton_add_singleton {α : Type u_1} {a b : α} [has_add α] :

{a} + {b} = {a + b}

source

@[protected, instance]

def set.add_zero_class {α : Type u_1} [add_zero_class α] :

add_zero_class (set α)

source

@[protected, instance]

def set.mul_one_class {α : Type u_1} [mul_one_class α] :

mul_one_class (set α)

Equations

set.mul_one_class = {one := 1, mul := has_mul.mul set.has_mul, one_mul := _, mul_one := _}

source

@[protected, instance]

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

add_semigroup (set α)

source

@[protected, instance]

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

semigroup (set α)

Equations

set.semigroup = {mul := has_mul.mul set.has_mul, mul_assoc := _}

source

@[protected, instance]

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

monoid (set α)

Equations

set.monoid = {mul := semigroup.mul set.semigroup, mul_assoc := _, one := mul_one_class.one set.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (set α)), npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

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

add_monoid (set α)

source

@[protected]

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

s * t = t * s

source

@[protected]

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

s + t = t + s

source

@[protected, instance]

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

comm_monoid (set α)

Equations

set.comm_monoid = {mul := monoid.mul set.monoid, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := npow set.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

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

add_comm_monoid (set α)

source

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

is_mul_hom singleton

source

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

is_add_hom singleton

source

@[simp]

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

∅ * s = ∅

source

@[simp]

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

∅ + s = ∅

source

@[simp]

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

s + ∅ = ∅

source

@[simp]

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

s * ∅ = ∅

source

theorem set.add_subset_add {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_add α] (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) :

s₁ + s₂ ⊆ t₁ + t₂

source

theorem set.mul_subset_mul {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_mul α] (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) :

s₁ * s₂ ⊆ t₁ * t₂

source

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

(s ∪ t) * u = s * u ∪ t * u

source

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

s ∪ t + u = s + u ∪ (t + u)

source

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

s * (t ∪ u) = s * t ∪ s * u

source

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

s + (t ∪ u) = s + t ∪ (s + u)

source

theorem set.Union_mul_left_image {α : Type u_1} {s t : set α} [has_mul α] :

(⋃ (a : α) (H : a ∈ s), (λ (x : α), a * x) '' t) = s * t

source

theorem set.Union_add_left_image {α : Type u_1} {s t : set α} [has_add α] :

(⋃ (a : α) (H : a ∈ s), (λ (x : α), a + x) '' t) = s + t

source

theorem set.Union_mul_right_image {α : Type u_1} {s t : set α} [has_mul α] :

(⋃ (a : α) (H : a ∈ t), (λ (x : α), x * a) '' s) = s * t

source

theorem set.Union_add_right_image {α : Type u_1} {s t : set α} [has_add α] :

(⋃ (a : α) (H : a ∈ t), (λ (x : α), x + a) '' s) = s + t

source

@[simp]

theorem set.univ_add_univ {α : Type u_1} [add_monoid α] :

set.univ + set.univ = set.univ

source

@[simp]

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

set.univ * set.univ = set.univ

source

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

α →* set α

singleton is a monoid hom.

Equations

set.singleton_hom = {to_fun := singleton set.has_singleton, map_one' := _, map_mul' := _}

source

def set.singleton_add_hom {α : Type u_1} [add_monoid α] :

α →+ set α

singleton is an add monoid hom

source

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

s.nonempty → t.nonempty → (s + t).nonempty

source

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

s.nonempty → t.nonempty → (s * t).nonempty

source

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

(s * t).finite

source

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

(s + t).finite

source

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

fintype ↥(s + t)

addition preserves finiteness

source

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

fintype (↥s * t)

multiplication preserves finiteness

Equations

s.fintype_mul t = set.fintype_image2 (λ (a b : α), a * b) s t

source

theorem set.bdd_above_add {α : Type u_1} [ordered_add_comm_monoid α] {A B : set α} :

bdd_above A → bdd_above B → bdd_above (A + B)

source

theorem set.bdd_above_mul {α : Type u_1} [ordered_comm_monoid α] {A B : set α} :

bdd_above A → bdd_above B → bdd_above (A * B)

Properties about inversion #

source

@[protected, instance]

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

has_neg (set α)

source

@[protected, instance]

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

has_inv (set α)

Equations

set.has_inv = {inv := set.preimage has_inv.inv}

source

@[simp]

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

a ∈ s⁻¹ ↔ a⁻¹ ∈ s

source

@[simp]

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

a ∈ -s ↔ -a ∈ s

source

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

a⁻¹ ∈ s⁻¹ ↔ a ∈ s

source

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

-a ∈ -s ↔ a ∈ s

source

@[simp]

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

has_inv.inv ⁻¹' s = s⁻¹

source

@[simp]

theorem set.neg_preimage {α : Type u_1} {s : set α} [has_neg α] :

has_neg.neg ⁻¹' s = -s

source

@[simp]

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

has_inv.inv '' s = s⁻¹

source

@[simp]

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

has_neg.neg '' s = -s

source

@[simp]

theorem set.inter_neg {α : Type u_1} {s t : set α} [has_neg α] :

-(s ∩ t) = -s ∩ -t

source

@[simp]

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

(s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

source

@[simp]

theorem set.union_neg {α : Type u_1} {s t : set α} [has_neg α] :

-(s ∪ t) = -s ∪ -t

source

@[simp]

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

(s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹

source

@[simp]

theorem set.compl_neg {α : Type u_1} {s : set α} [has_neg α] :

-sᶜ = (-s)ᶜ

source

@[simp]

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

sᶜ ⁻¹ = s⁻¹ ᶜ

source

@[protected, simp]

theorem set.neg_neg {α : Type u_1} {s : set α} [add_group α] :

--s = s

source

@[protected, simp]

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

s⁻¹ ⁻¹ = s

source

@[protected, simp]

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

-set.univ = set.univ

source

@[protected, simp]

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

set.univ ⁻¹ = set.univ

source

@[simp]

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

-s ⊆ -t ↔ s ⊆ t

source

@[simp]

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

s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t

source

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

s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

source

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

-s ⊆ t ↔ s ⊆ -t

source

theorem set.finite.inv {α : Type u_1} [group α] {s : set α} (hs : s.finite) :

s⁻¹.finite

source

theorem set.finite.neg {α : Type u_1} [add_group α] {s : set α} (hs : s.finite) :

(-s).finite

Properties about scalar multiplication #

source

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

set.has_scalar_set = {smul := λ (a : α), set.image (has_scalar.smul a)}

source

@[simp]

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

(λ (x : β), a • x) '' t = a • t

source

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

source

theorem set.smul_mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {y : β} [has_scalar α β] {t : set β} (hy : y ∈ t) :

a • y ∈ a • t

source

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

a • (s ∪ t) = a • s ∪ a • t

source

@[simp]

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

a • ∅ = ∅

source

theorem set.smul_set_mono {α : Type u_1} {β : Type u_2} {a : α} [has_scalar α β] {s t : set β} (h : s ⊆ t) :

a • s ⊆ a • t

source

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

set.has_scalar = {smul := set.image2 has_scalar.smul}

source

@[simp]

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

set.image2 has_scalar.smul s t = s • t

source

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

source

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

source

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)

source

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

{a} • t = a • t

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

source

@[protected, instance]

def set.set_semiring.inhabited (α : Type u_1) :

inhabited (set.set_semiring α)

source

def set.set_semiring (α : Type u_1) :

Type u_1

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

Equations

set.set_semiring α = set α

source

@[protected]

def set.up {α : Type u_1} (s : set α) :

set.set_semiring α

The identitiy function set α → set_semiring α.

Equations

s.up = s

source

@[protected]

def set.set_semiring.down {α : Type u_1} (s : set.set_semiring α) :

set α

The identitiy function set_semiring α → set α.

Equations

s.down = s

source

@[protected, simp]

theorem set.down_up {α : Type u_1} {s : set α} :

s.up.down = s

source

@[protected, simp]

theorem set.up_down {α : Type u_1} {s : set.set_semiring α} :

s.down.up = s

source

@[protected, instance]

def set.set_semiring.add_comm_monoid {α : Type u_1} :

add_comm_monoid (set.set_semiring α)

Equations

set.set_semiring.add_comm_monoid = {add := λ (s t : set.set_semiring α), s ∪ t, add_assoc := _, zero := ∅, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ∅ (λ (s t : set.set_semiring α), s ∪ t) set.empty_union set.union_empty, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def set.set_semiring.mul_zero_class {α : Type u_1} [has_mul α] :

mul_zero_class (set.set_semiring α)

Equations

set.set_semiring.mul_zero_class = {mul := has_mul.mul set.has_mul, zero := add_comm_monoid.zero set.set_semiring.add_comm_monoid, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def set.set_semiring.distrib {α : Type u_1} [has_mul α] :

distrib (set.set_semiring α)

Equations

set.set_semiring.distrib = {mul := has_mul.mul set.has_mul, add := add_comm_monoid.add set.set_semiring.add_comm_monoid, left_distrib := _, right_distrib := _}

source

@[protected, instance]

def set.set_semiring.mul_zero_one_class {α : Type u_1} [mul_one_class α] :

mul_zero_one_class (set.set_semiring α)

Equations

set.set_semiring.mul_zero_one_class = {one := mul_one_class.one set.mul_one_class, mul := mul_zero_class.mul set.set_semiring.mul_zero_class, one_mul := _, mul_one := _, zero := mul_zero_class.zero set.set_semiring.mul_zero_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def set.set_semiring.semigroup_with_zero {α : Type u_1} [semigroup α] :

semigroup_with_zero (set.set_semiring α)

Equations

set.set_semiring.semigroup_with_zero = {mul := mul_zero_class.mul set.set_semiring.mul_zero_class, mul_assoc := _, zero := mul_zero_class.zero set.set_semiring.mul_zero_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

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

semiring (set.set_semiring α)

Equations

set.set_semiring.semiring = {add := add_comm_monoid.add set.set_semiring.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero set.set_semiring.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul set.set_semiring.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := distrib.mul set.set_semiring.distrib, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := npow set.monoid, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

@[protected, instance]

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

comm_semiring (set.set_semiring α)

Equations

set.set_semiring.comm_semiring = {add := semiring.add set.set_semiring.semiring, add_assoc := _, zero := semiring.zero set.set_semiring.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul set.set_semiring.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul set.comm_monoid, mul_assoc := _, one := comm_monoid.one set.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow set.comm_monoid, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

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

set.mul_action_set = {to_has_scalar := {smul := has_scalar.smul set.has_scalar_set}, one_smul := _, mul_smul := _}

source

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

source

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

source

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

source

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)

source

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

set.set_semiring α →+* set.set_semiring β

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

Equations

set.image_hom f = {to_fun := set.image ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem zero_smul_set {α : Type u_1} {β : Type u_2} [semiring α] [add_comm_monoid β] [module α β] {s : set β} (h : s.nonempty) :

0 • s = 0

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

source

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

source

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

source

@[protected, instance]

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

has_add (finset α)

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

source

@[protected, instance]

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

has_mul (finset α)

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

Equations

finset.has_mul = {mul := λ (s t : finset α), finset.image (λ (p : α × α), (p.fst) * p.snd) (s.product t)}

source

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)

source

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)

source

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

source

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

source

@[simp]

theorem finset.coe_add {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :

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

source

@[simp, norm_cast]

theorem finset.coe_mul {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :

↑s * t = (↑s) * ↑t

source

theorem finset.mul_mem_mul {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} {x y : α} (hx : x ∈ s) (hy : y ∈ t) :

x * y ∈ s * t

source

theorem finset.add_mem_add {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} {x y : α} (hx : x ∈ s) (hy : y ∈ t) :

x + y ∈ s + t

source

theorem finset.add_card_le {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :

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

source

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

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

source

theorem finset.subset_mul {M : Type u_1} [monoid M] {S S' : set M} {U : finset M} (f : ↑U ⊆ S * S') :

∃ (T T' : finset M), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ U ⊆ T * T'

A finite set U contained in the product of two sets S * S' is also contained in the product of two finite sets T * T' ⊆ S * S'.

source

theorem finset.subset_add {M : Type u_1} [add_monoid M] {S S' : set M} {U : finset M} (f : ↑U ⊆ S + S') :

∃ (T T' : finset M), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ U ⊆ T + T'

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in group_theory.submonoid.basic, but currently we cannot because that file is imported by this.

source

theorem submonoid.mul_subset {M : Type u_1} [monoid M] {s t : set M} {S : submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s * t ⊆ ↑S

source

theorem add_submonoid.add_subset {M : Type u_1} [add_monoid M] {s t : set M} {S : add_submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s + t ⊆ ↑S

source

theorem add_submonoid.add_subset_closure {M : Type u_1} [add_monoid M] {s t u : set M} (hs : s ⊆ u) (ht : t ⊆ u) :

s + t ⊆ ↑(add_submonoid.closure u)

source

theorem submonoid.mul_subset_closure {M : Type u_1} [monoid M] {s t u : set M} (hs : s ⊆ u) (ht : t ⊆ u) :

s * t ⊆ ↑(submonoid.closure u)

source

theorem add_submonoid.coe_add_self_eq {M : Type u_1} [add_monoid M] (s : add_submonoid M) :

↑s + ↑s = ↑s

source

theorem submonoid.coe_mul_self_eq {M : Type u_1} [monoid M] (s : submonoid M) :

(↑s) * ↑s = ↑s

source

theorem add_submonoid.closure_add_le {M : Type u_1} [add_monoid M] (S T : set M) :

add_submonoid.closure (S + T) ≤ add_submonoid.closure S ⊔ add_submonoid.closure T

source

theorem submonoid.closure_mul_le {M : Type u_1} [monoid M] (S T : set M) :

submonoid.closure (S * T) ≤ submonoid.closure S ⊔ submonoid.closure T

source

theorem add_submonoid.sup_eq_closure {M : Type u_1} [add_monoid M] (H K : add_submonoid M) :

H ⊔ K = add_submonoid.closure (↑H + ↑K)

source

theorem submonoid.sup_eq_closure {M : Type u_1} [monoid M] (H K : submonoid M) :

H ⊔ K = submonoid.closure ((↑H) * ↑K)

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

Implementation notes #

Tags #

Properties about 1 #

Properties about multiplication #

Properties about inversion #

Properties about scalar multiplication #

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

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