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.

ink

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

• SetSemiring α = Set α

ink

noncomputable instance instInhabitedSetSemiring (α : Type u_1) : Inhabited (SetSemiring α)

Equations

• instInhabitedSetSemiring α = inferInstance

ink

instance instPartialOrderSetSemiring (α : Type u_1) : PartialOrder (SetSemiring α)

Equations

• instPartialOrderSetSemiring α = inferInstance

ink

instance instOrderBotSetSemiringToLEToPreorderInstPartialOrderSetSemiring (α : Type u_1) : OrderBot (SetSemiring α)

Equations

• instOrderBotSetSemiringToLEToPreorderInstPartialOrderSetSemiring α = inferInstance

ink

def Set.up {α : Type u_1} : Set α ≃ SetSemiring α

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

Equations

• Set.up = Equiv.refl (Set α)

ink

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

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

Equations

• SetSemiring.down = Equiv.refl (SetSemiring α)

ink

@[simp]

theorem SetSemiring.down_up {α : Type u_1} (s : Set α) : ↑SetSemiring.down (↑Set.up s) = s

ink

@[simp]

theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) : ↑Set.up (↑SetSemiring.down s) = s

ink

theorem SetSemiring.up_le_up {α : Type u_1} {s : Set α} {t : Set α} : ↑Set.up s ≤ ↑Set.up t ↔ s ⊆ t

ink

theorem SetSemiring.up_lt_up {α : Type u_1} {s : Set α} {t : Set α} : ↑Set.up s < ↑Set.up t ↔ s ⊂ t

ink

@[simp]

theorem SetSemiring.down_subset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} : ↑SetSemiring.down s ⊆ ↑SetSemiring.down t ↔ s ≤ t

ink

@[simp]

theorem SetSemiring.down_ssubset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} : ↑SetSemiring.down s ⊂ ↑SetSemiring.down t ↔ s < t

ink

instance SetSemiring.instAddCommMonoidSetSemiring {α : Type u_1} : AddCommMonoid (SetSemiring α)

Equations

• SetSemiring.instAddCommMonoidSetSemiring = AddCommMonoid.mk (_ : ∀ (a b : Set α), a ∪ b = b ∪ a)

ink

theorem SetSemiring.zero_def {α : Type u_1} : 0 = ↑Set.up ∅

ink

@[simp]

theorem SetSemiring.down_zero {α : Type u_1} : ↑SetSemiring.down 0 = ∅

ink

@[simp]

theorem Set.up_empty {α : Type u_1} : ↑Set.up ∅ = 0

ink

theorem SetSemiring.add_def {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) : s + t = ↑Set.up (↑SetSemiring.down s ∪ ↑SetSemiring.down t)

ink

@[simp]

theorem SetSemiring.down_add {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) : ↑SetSemiring.down (s + t) = ↑SetSemiring.down s ∪ ↑SetSemiring.down t

ink

@[simp]

theorem Set.up_union {α : Type u_1} (s : Set α) (t : Set α) : ↑Set.up (s ∪ t) = ↑Set.up s + ↑Set.up t

ink

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

• @SetSemiring.covariantClass_add = @SetSemiring.covariantClass_add.proof_1

ink

instance SetSemiring.instNonUnitalNonAssocSemiringSetSemiring {α : Type u_1} [inst : Mul α] : NonUnitalNonAssocSemiring (SetSemiring α)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem SetSemiring.mul_def {α : Type u_1} [inst : Mul α] (s : SetSemiring α) (t : SetSemiring α) : s * t = ↑Set.up (↑SetSemiring.down s * ↑SetSemiring.down t)

ink

@[simp]

theorem SetSemiring.down_mul {α : Type u_1} [inst : Mul α] (s : SetSemiring α) (t : SetSemiring α) : ↑SetSemiring.down (s * t) = ↑SetSemiring.down s * ↑SetSemiring.down t

ink

@[simp]

theorem Set.up_mul {α : Type u_1} [inst : Mul α] (s : Set α) (t : Set α) : ↑Set.up (s * t) = ↑Set.up s * ↑Set.up t

ink

instance SetSemiring.instNoZeroDivisorsSetSemiringToMulInstNonUnitalNonAssocSemiringSetSemiringToZeroToMulZeroClass {α : Type u_1} [inst : Mul α] : NoZeroDivisors (SetSemiring α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• @SetSemiring.covariantClass_mul_left = @SetSemiring.covariantClass_mul_left.proof_1

ink

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

Equations

• @SetSemiring.covariantClass_mul_right = @SetSemiring.covariantClass_mul_right.proof_1

ink

noncomputable instance SetSemiring.instOneSetSemiring {α : Type u_1} [inst : One α] : One (SetSemiring α)

Equations

• SetSemiring.instOneSetSemiring = { one := ↑Set.up 1 }

ink

theorem SetSemiring.one_def {α : Type u_1} [inst : One α] : 1 = ↑Set.up 1

ink

@[simp]

theorem SetSemiring.down_one {α : Type u_1} [inst : One α] : ↑SetSemiring.down 1 = 1

ink

@[simp]

theorem Set.up_one {α : Type u_1} [inst : One α] : ↑Set.up 1 = 1

ink

instance SetSemiring.instNonAssocSemiringSetSemiring {α : Type u_1} [inst : MulOneClass α] : NonAssocSemiring (SetSemiring α)

Equations

• SetSemiring.instNonAssocSemiringSetSemiring = let src := inferInstance; let src_1 := Set.mulOneClass; NonAssocSemiring.mk (_ : ∀ (a : Set α), 1 * a = a) (_ : ∀ (a : Set α), a * 1 = a)

ink

instance SetSemiring.instNonUnitalSemiringSetSemiring {α : Type u_1} [inst : Semigroup α] : NonUnitalSemiring (SetSemiring α)

Equations

• SetSemiring.instNonUnitalSemiringSetSemiring = let src := inferInstance; let src_1 := Set.semigroup; NonUnitalSemiring.mk (_ : ∀ (a b c : Set α), a * b * c = a * (b * c))

ink

instance SetSemiring.instIdemSemiringSetSemiring {α : Type u_1} [inst : Monoid α] : IdemSemiring (SetSemiring α)

Equations

• SetSemiring.instIdemSemiringSetSemiring = let src := inferInstance; let src_1 := inferInstance; let src_2 := inferInstance; IdemSemiring.mk ⊥ (_ : ∀ (a : Set α), ⊥ ≤ a)

ink

instance SetSemiring.instNonUnitalCommSemiringSetSemiring {α : Type u_1} [inst : CommSemigroup α] : NonUnitalCommSemiring (SetSemiring α)

Equations

• SetSemiring.instNonUnitalCommSemiringSetSemiring = let src := inferInstance; let src_1 := Set.commSemigroup; NonUnitalCommSemiring.mk (_ : ∀ (a b : Set α), a * b = b * a)

ink

instance SetSemiring.instIdemCommSemiringSetSemiring {α : Type u_1} [inst : CommMonoid α] : IdemCommSemiring (SetSemiring α)

Equations

• SetSemiring.instIdemCommSemiringSetSemiring = let src := inferInstance; let src_1 := inferInstance; IdemCommSemiring.mk IdemSemiring.bot (_ : ∀ (a : SetSemiring α), IdemSemiring.bot ≤ a)

ink

instance SetSemiring.instCommMonoidSetSemiring {α : Type u_1} [inst : CommMonoid α] : CommMonoid (SetSemiring α)

Equations

• SetSemiring.instCommMonoidSetSemiring = let src := inferInstance; let src_1 := Set.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Set α), a * b = b * a)

ink

instance SetSemiring.instCanonicallyOrderedCommSemiringSetSemiring {α : Type u_1} [inst : CommMonoid α] : CanonicallyOrderedCommSemiring (SetSemiring α)

Equations

• One or more equations did not get rendered due to their size.

ink

def SetSemiring.imageHom {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst : MulOneClass β] (f : α →* β) : SetSemiring α →+* SetSemiring β

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.

ink

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)

ink

@[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

ink

@[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)