mathlib3 documentation

data.set.semiring

Sets as a semiring under union #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[protected, instance]
@[protected, instance]
@[protected]
def set.up {α : Type u_1} :

The identity function set α → set_semiring α.

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

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 α} :
theorem set_semiring.up_lt_up {α : Type u_1} {s t : set α} :
theorem set_semiring.zero_def {α : Type u_1} :
@[simp]
@[simp]
theorem set.up_empty {α : Type u_1} :
@[simp]
theorem set.up_union {α : Type u_1} (s t : set α) :
@[simp]
theorem set.up_mul {α : Type u_1} [has_mul α] (s t : set α) :
@[protected, instance]
@[protected, instance]
def set_semiring.has_one {α : Type u_1} [has_one α] :
Equations
theorem set_semiring.one_def {α : Type u_1} [has_one α] :
@[simp]
theorem set_semiring.down_one {α : Type u_1} [has_one α] :
@[simp]
theorem set.up_one {α : Type u_1} [has_one α] :
@[protected, instance]
Equations
def set_semiring.image_hom {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) :

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

Equations
@[simp]
theorem set.up_image {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (s : set α) :