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".
Equations
- SetSemiring α = Set α
Equations
- instInhabitedSetSemiring α = inferInstance
Equations
- instPartialOrderSetSemiring α = inferInstance
instance
instOrderBotSetSemiringToLEToPreorderInstPartialOrderSetSemiring
(α : Type u_1)
:
OrderBot (SetSemiring α)
Equations
- instOrderBotSetSemiringToLEToPreorderInstPartialOrderSetSemiring α = inferInstance
The identity function Set α → SetSemiring α→ SetSemiring α
.
Equations
- Set.up = Equiv.refl (Set α)
The identity function SetSemiring α → Set α→ Set α
.
Equations
- SetSemiring.down = Equiv.refl (SetSemiring α)
@[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
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SetSemiring.down_mul
{α : Type u_1}
[inst : Mul α]
(s : SetSemiring α)
(t : SetSemiring α)
:
instance
SetSemiring.instNoZeroDivisorsSetSemiringToMulInstNonUnitalNonAssocSemiringSetSemiringToZeroToMulZeroClass
{α : Type u_1}
[inst : Mul α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
SetSemiring.covariantClass_mul_left
{α : Type u_1}
[inst : 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}
[inst : Mul α]
:
CovariantClass (SetSemiring α) (SetSemiring α) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
noncomputable instance
SetSemiring.instOneSetSemiring
{α : Type u_1}
[inst : One α]
:
One (SetSemiring α)
Equations
- SetSemiring.instOneSetSemiring = { one := ↑Set.up 1 }
Equations
- SetSemiring.instIdemCommSemiringSetSemiring = let src := inferInstance; let src_1 := inferInstance; IdemCommSemiring.mk IdemSemiring.bot (_ : ∀ (a : SetSemiring α), IdemSemiring.bot ≤ a)
instance
SetSemiring.instCanonicallyOrderedCommSemiringSetSemiring
{α : Type u_1}
[inst : CommMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
def
SetSemiring.imageHom
{α : Type u_1}
{β : Type u_2}
[inst : MulOneClass α]
[inst : MulOneClass β]
(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 : MulOneClass α]
[inst : 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}
[inst : MulOneClass α]
[inst : 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}
[inst : MulOneClass α]
[inst : MulOneClass β]
(f : α →* β)
(s : Set α)
:
↑Set.up (↑f '' s) = ↑(SetSemiring.imageHom f) (↑Set.up s)