# mathlibdocumentation

data.set.semiring

# Sets as a semiring under union #

This file defines set_semiring α, an alias of set α, which we endow with ∪ as addition and pointwise * as multiplication. If α is a (commutative) monoid, set_semiring α is a (commutative) semiring.

@[protected, instance]
def set_semiring.order_bot (α : Type u_1) :
@[protected, instance]
def set_semiring.inhabited (α : Type u_1) :
@[protected, instance]
def set_semiring.partial_order (α : Type u_1) :
def 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
Instances for set_semiring
@[protected]
def set.up {α : Type u_1} :
set α

The identity function set α → set_semiring α.

Equations
@[protected]
def set_semiring.down {α : Type u_1} :
set α

The identity function set_semiring α → set α.

Equations
@[protected, simp]
theorem set_semiring.down_up {α : Type u_1} (s : set α) :
@[protected, simp]
theorem set_semiring.up_down {α : Type u_1} (s : set_semiring α) :
theorem set_semiring.up_le_up {α : Type u_1} {s t : set α} :
s t
theorem set_semiring.up_lt_up {α : Type u_1} {s t : set α} :
< s t
@[simp]
theorem set_semiring.down_subset_down {α : Type u_1} {s t : set_semiring α} :
s t
@[simp]
theorem set_semiring.down_ssubset_down {α : Type u_1} {s t : set_semiring α} :
s < t
@[protected, instance]
def set_semiring.add_comm_monoid {α : Type u_1} :
Equations
@[protected, instance]
def set_semiring.covariant_class_add {α : Type u_1} :
@[protected, instance]
Equations
@[protected, instance]
def set_semiring.no_zero_divisors {α : Type u_1} [has_mul α] :
@[protected, instance]
def set_semiring.covariant_class_mul_left {α : Type u_1} [has_mul α] :
@[protected, instance]
def set_semiring.covariant_class_mul_right {α : Type u_1} [has_mul α] :
@[protected, instance]
def set_semiring.non_assoc_semiring {α : Type u_1}  :
Equations
@[protected, instance]
def set_semiring.non_unital_semiring {α : Type u_1} [semigroup α] :
Equations
@[protected, instance]
def set_semiring.semiring {α : Type u_1} [monoid α] :
Equations
@[protected, instance]
def set_semiring.non_unital_comm_semiring {α : Type u_1}  :
Equations
@[protected, instance]
Equations
def set_semiring.image_hom {α : Type u_1} {β : Type u_2} (f : α →* β) :

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

Equations