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.
An alias for Set α
, which has a semiring structure given by ∪
as "addition" and pointwise
multiplication *
as "multiplication".
Instances For
instance
instOrderBotSetSemiringToLEToPreorderInstPartialOrderSetSemiring
(α : Type u_3)
:
OrderBot (SetSemiring α)
The identity function Set α → SetSemiring α
.
Instances For
The identity function SetSemiring α → Set α
.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
instance
SetSemiring.covariantClass_add
{α : Type u_1}
:
CovariantClass (SetSemiring α) (SetSemiring α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
@[simp]
instance
SetSemiring.covariantClass_mul_left
{α : Type u_1}
[Mul α]
:
CovariantClass (SetSemiring α) (SetSemiring α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
instance
SetSemiring.covariantClass_mul_right
{α : Type u_1}
[Mul α]
:
CovariantClass (SetSemiring α) (SetSemiring α) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
def
SetSemiring.imageHom
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
:
The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.
Instances For
theorem
SetSemiring.imageHom_def
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : SetSemiring α)
:
↑(SetSemiring.imageHom f) s = ↑Set.up (↑f '' ↑SetSemiring.down s)
@[simp]
theorem
SetSemiring.down_imageHom
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : SetSemiring α)
:
↑SetSemiring.down (↑(SetSemiring.imageHom f) s) = ↑f '' ↑SetSemiring.down s
@[simp]
theorem
Set.up_image
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : Set α)
:
↑Set.up (↑f '' s) = ↑(SetSemiring.imageHom f) (↑Set.up s)