# Documentation

Mathlib.Data.Set.Semiring

# Sets as a semiring under union #

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

def SetSemiring (α : 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
noncomputable instance instInhabitedSetSemiring (α : Type u_1) :
Equations
• = inferInstance
instance instPartialOrderSetSemiring (α : Type u_1) :
Equations
• = inferInstance
def Set.up {α : Type u_1} :
Set α

The identity function Set α → SetSemiring α→ SetSemiring α.

Equations
def SetSemiring.down {α : Type u_1} :
Set α

The identity function SetSemiring α → Set α→ Set α.

Equations
• SetSemiring.down =
@[simp]
theorem SetSemiring.down_up {α : Type u_1} (s : Set α) :
SetSemiring.down (Set.up s) = s
@[simp]
theorem SetSemiring.up_down {α : Type u_1} (s : ) :
Set.up (SetSemiring.down s) = s
theorem SetSemiring.up_le_up {α : Type u_1} {s : Set α} {t : Set α} :
Set.up s Set.up t s t
theorem SetSemiring.up_lt_up {α : Type u_1} {s : Set α} {t : Set α} :
Set.up s < Set.up t s t
@[simp]
theorem SetSemiring.down_subset_down {α : Type u_1} {s : } {t : } :
SetSemiring.down s SetSemiring.down t s t
@[simp]
theorem SetSemiring.down_ssubset_down {α : Type u_1} {s : } {t : } :
SetSemiring.down s SetSemiring.down t s < t
Equations
theorem SetSemiring.zero_def {α : Type u_1} :
0 = Set.up
@[simp]
theorem SetSemiring.down_zero {α : Type u_1} :
SetSemiring.down 0 =
@[simp]
theorem Set.up_empty {α : Type u_1} :
Set.up = 0
theorem SetSemiring.add_def {α : Type u_1} (s : ) (t : ) :
s + t = Set.up (SetSemiring.down s SetSemiring.down t)
@[simp]
theorem SetSemiring.down_add {α : Type u_1} (s : ) (t : ) :
SetSemiring.down (s + t) = SetSemiring.down s SetSemiring.down t
@[simp]
theorem Set.up_union {α : Type u_1} (s : Set α) (t : Set α) :
Set.up (s t) = Set.up s + Set.up t
instance SetSemiring.covariantClass_add {α : Type u_1} :
CovariantClass () () (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
Equations
• One or more equations did not get rendered due to their size.
theorem SetSemiring.mul_def {α : Type u_1} [inst : Mul α] (s : ) (t : ) :
s * t = Set.up (SetSemiring.down s * SetSemiring.down t)
@[simp]
theorem SetSemiring.down_mul {α : Type u_1} [inst : Mul α] (s : ) (t : ) :
SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t
@[simp]
theorem Set.up_mul {α : Type u_1} [inst : Mul α] (s : Set α) (t : Set α) :
Set.up (s * t) = Set.up s * Set.up t
Equations
• One or more equations did not get rendered due to their size.
instance SetSemiring.covariantClass_mul_left {α : Type u_1} [inst : Mul α] :
CovariantClass () () (fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
instance SetSemiring.covariantClass_mul_right {α : Type u_1} [inst : Mul α] :
CovariantClass () () (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
noncomputable instance SetSemiring.instOneSetSemiring {α : Type u_1} [inst : One α] :
One ()
Equations
• SetSemiring.instOneSetSemiring = { one := Set.up 1 }
theorem SetSemiring.one_def {α : Type u_1} [inst : One α] :
1 = Set.up 1
@[simp]
theorem SetSemiring.down_one {α : Type u_1} [inst : One α] :
SetSemiring.down 1 = 1
@[simp]
theorem Set.up_one {α : Type u_1} [inst : One α] :
Set.up 1 = 1
instance SetSemiring.instNonAssocSemiringSetSemiring {α : Type u_1} [inst : ] :
Equations
• SetSemiring.instNonAssocSemiringSetSemiring = let src := inferInstance; let src_1 := Set.mulOneClass; NonAssocSemiring.mk (_ : ∀ (a : Set α), 1 * a = a) (_ : ∀ (a : Set α), a * 1 = a)
instance SetSemiring.instNonUnitalSemiringSetSemiring {α : Type u_1} [inst : ] :
Equations
• SetSemiring.instNonUnitalSemiringSetSemiring = let src := inferInstance; let src_1 := Set.semigroup; NonUnitalSemiring.mk (_ : ∀ (a b c : Set α), a * b * c = a * (b * c))
instance SetSemiring.instIdemSemiringSetSemiring {α : Type u_1} [inst : ] :
Equations
• SetSemiring.instIdemSemiringSetSemiring = let src := inferInstance; let src_1 := inferInstance; let src_2 := inferInstance; IdemSemiring.mk (_ : ∀ (a : Set α), a)
Equations
• SetSemiring.instNonUnitalCommSemiringSetSemiring = let src := inferInstance; let src_1 := Set.commSemigroup; NonUnitalCommSemiring.mk (_ : ∀ (a b : Set α), a * b = b * a)
instance SetSemiring.instIdemCommSemiringSetSemiring {α : Type u_1} [inst : ] :
Equations
• SetSemiring.instIdemCommSemiringSetSemiring = let src := inferInstance; let src_1 := inferInstance; IdemCommSemiring.mk IdemSemiring.bot (_ : ∀ (a : ), IdemSemiring.bot a)
instance SetSemiring.instCommMonoidSetSemiring {α : Type u_1} [inst : ] :
Equations
• SetSemiring.instCommMonoidSetSemiring = let src := inferInstance; let src_1 := Set.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Set α), a * b = b * a)
Equations
• One or more equations did not get rendered due to their size.
def SetSemiring.imageHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →* β) :

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

Equations
• One or more equations did not get rendered due to their size.
theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →* β) (s : ) :
↑() s = Set.up (f '' SetSemiring.down s)
@[simp]
theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →* β) (s : ) :
SetSemiring.down (↑() s) = f '' SetSemiring.down s
@[simp]
theorem Set.up_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →* β) (s : Set α) :
Set.up (f '' s) = ↑() (Set.up s)