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 an idempotent (commutative) semiring.

def SetSemiring (α : Type u_4) : Type u_4

An alias for Set α, which has a semiring structure given by ∪ as "addition" and pointwise multiplication * as "multiplication".

Equations

• SetSemiring α = Set α

@[instance_reducible]

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

Equations

• instInhabitedSetSemiring α = { default := instInhabitedSetSemiring._aux_1 α }

@[instance_reducible]

instance instCompleteAtomicBooleanAlgebraSetSemiring (α : Type u_1) : CompleteAtomicBooleanAlgebra (SetSemiring α)

Equations

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

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

The identity equivalence between Set α and SetSemiring α.

Equations

• SetSemiring.ofSet = Equiv.refl (Set α)

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

The identity equivalence between SetSemiring α and Set α.

Equations

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

@[simp]

theorem SetSemiring.toSet_ofSet {α : Type u_1} (s : Set α) : toSet (ofSet s) = s

@[simp]

theorem SetSemiring.ofSet_toSet {α : Type u_1} (s : SetSemiring α) : ofSet (toSet s) = s

@[simp]

theorem SetSemiring.ofSet_le_ofSet {α : Type u_1} {s t : Set α} : ofSet s ≤ ofSet t ↔ s ⊆ t

@[simp]

theorem SetSemiring.ofSet_lt_ofSet {α : Type u_1} {s t : Set α} : ofSet s < ofSet t ↔ s ⊂ t

@[simp]

theorem SetSemiring.toSet_subset_toSet {α : Type u_1} {s t : SetSemiring α} : toSet s ⊆ toSet t ↔ s ≤ t

@[simp]

theorem SetSemiring.toSet_ssubset_toSet {α : Type u_1} {s t : SetSemiring α} : toSet s ⊂ toSet t ↔ s < t

@[simp]

theorem SetSemiring.symm_toSet {α : Type u_1} : toSet.symm = ofSet

@[simp]

theorem SetSemiring.symm_ofSet {α : Type u_1} : ofSet.symm = toSet

@[instance_reducible]

instance SetSemiring.instZero {α : Type u_1} : Zero (SetSemiring α)

Equations

• SetSemiring.instZero = { zero := SetSemiring.ofSet ∅ }

@[instance_reducible]

instance SetSemiring.instAdd {α : Type u_1} : Add (SetSemiring α)

Equations

• SetSemiring.instAdd = { add := fun (s t : SetSemiring α) => SetSemiring.ofSet (SetSemiring.toSet s ∪ SetSemiring.toSet t) }

theorem SetSemiring.zero_def {α : Type u_1} : 0 = ofSet ∅

@[simp]

theorem SetSemiring.toSet_zero {α : Type u_1} : toSet 0 = ∅

@[simp]

theorem SetSemiring.ofSet_empty {α : Type u_1} : ofSet ∅ = 0

theorem SetSemiring.add_def {α : Type u_1} (s t : SetSemiring α) : s + t = ofSet (toSet s ∪ toSet t)

@[simp]

theorem SetSemiring.toSet_add {α : Type u_1} (s t : SetSemiring α) : toSet (s + t) = toSet s ∪ toSet t

@[simp]

theorem SetSemiring.ofSet_union {α : Type u_1} (s t : Set α) : ofSet (s ∪ t) = ofSet s + ofSet t

@[instance_reducible]

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

Equations

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

instance SetSemiring.instAddLeftMono {α : Type u_1} : AddLeftMono (SetSemiring α)

@[instance_reducible]

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

Equations

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

theorem SetSemiring.mul_def {α : Type u_1} [Mul α] (s t : SetSemiring α) : s * t = ofSet (toSet s * toSet t)

@[simp]

theorem SetSemiring.toSet_mul {α : Type u_1} [Mul α] (s t : SetSemiring α) : toSet (s * t) = toSet s * toSet t

@[simp]

theorem SetSemiring.ofSet_mul {α : Type u_1} [Mul α] (s t : Set α) : ofSet (s * t) = ofSet s * ofSet t

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

instance SetSemiring.instMulLeftMono {α : Type u_1} [Mul α] : MulLeftMono (SetSemiring α)

instance SetSemiring.instMulRightMono {α : Type u_1} [Mul α] : MulRightMono (SetSemiring α)

@[instance_reducible]

instance SetSemiring.instOne {α : Type u_1} [One α] : One (SetSemiring α)

Equations

• SetSemiring.instOne = { one := SetSemiring.ofSet 1 }

theorem SetSemiring.one_def {α : Type u_1} [One α] : 1 = ofSet 1

@[simp]

theorem SetSemiring.toSet_one {α : Type u_1} [One α] : toSet 1 = 1

@[simp]

theorem SetSemiring.ofSet_one {α : Type u_1} [One α] : ofSet 1 = 1

@[instance_reducible]

instance SetSemiring.instMulOneClass {α : Type u_1} [MulOneClass α] : MulOneClass (SetSemiring α)

Equations

• SetSemiring.instMulOneClass = { toOne := SetSemiring.instOne, toMul := SetSemiring.instNonUnitalNonAssocSemiring.toDistrib.toMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance SetSemiring.instSemigroup {α : Type u_1} [Semigroup α] : Semigroup (SetSemiring α)

Equations

• SetSemiring.instSemigroup = { toMul := SetSemiring.instNonUnitalNonAssocSemiring.toDistrib.toMul, mul_assoc := ⋯ }

@[instance_reducible]

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

Equations

• SetSemiring.instNonUnitalSemiringOfSemigroup = { toNonUnitalNonAssocSemiring := SetSemiring.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance SetSemiring.instCommSemigroup {α : Type u_1} [CommSemigroup α] : CommSemigroup (SetSemiring α)

Equations

• SetSemiring.instCommSemigroup = { toSemigroup := SetSemiring.instSemigroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• SetSemiring.instNonUnitalCommSemiringOfCommSemigroup = { toNonUnitalSemiring := SetSemiring.instNonUnitalSemiringOfSemigroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• SetSemiring.instCommMonoid = { toMonoid := SetSemiring.instIdemSemiringOfMonoid.toMonoid, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

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

instance SetSemiring.instCanonicallyOrderedAdd {α : Type u_1} : CanonicallyOrderedAdd (SetSemiring α)

instance SetSemiring.instIsOrderedRing {α : Type u_1} [CommMonoid α] : IsOrderedRing (SetSemiring α)

def SetSemiring.singletonMonoidHom {α : Type u_1} [Monoid α] : α →* SetSemiring α

If α is a monoid, the map that sends a : α to {a} is a monoid homomorphism.

Equations

• SetSemiring.singletonMonoidHom = { toFun := fun (a : α) => SetSemiring.ofSet {a}, map_one' := ⋯, map_mul' := ⋯ }

def SetSemiring.imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [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

• SetSemiring.imageHom f = { toFun := fun (s : SetSemiring α) => SetSemiring.ofSet (⇑f '' SetSemiring.toSet s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SetSemiring.imageHom_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (imageHom f) s = ofSet (⇑f '' toSet s)

@[simp]

theorem SetSemiring.imageHom_id {α : Type u_1} [MulOneClass α] : imageHom (MonoidHom.id α) = RingHom.id (SetSemiring α)

theorem SetSemiring.imageHom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) : imageHom (g.comp f) = (imageHom g).comp (imageHom f)

@[deprecated SetSemiring.ofSet (since := "2026-10-13")]

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

Alias of SetSemiring.ofSet.

---

The identity equivalence between Set α and SetSemiring α.

Equations

• @Set.up = @SetSemiring.ofSet

@[deprecated SetSemiring.toSet (since := "2026-10-13")]

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

Alias of SetSemiring.toSet.

---

The identity equivalence between SetSemiring α and Set α.

Equations

• @SetSemiring.down = @SetSemiring.toSet

@[deprecated SetSemiring.toSet_ofSet (since := "2026-10-13")]

theorem SetSemiring.down_up {α : Type u_1} (s : Set α) : toSet (ofSet s) = s

Alias of SetSemiring.toSet_ofSet.

@[deprecated SetSemiring.ofSet_toSet (since := "2026-10-13")]

theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) : ofSet (toSet s) = s

Alias of SetSemiring.ofSet_toSet.

@[deprecated SetSemiring.ofSet_le_ofSet (since := "2026-10-13")]

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

Alias of SetSemiring.ofSet_le_ofSet.

@[deprecated SetSemiring.ofSet_lt_ofSet (since := "2026-10-13")]

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

Alias of SetSemiring.ofSet_lt_ofSet.

@[deprecated SetSemiring.toSet_subset_toSet (since := "2026-10-13")]

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

Alias of SetSemiring.toSet_subset_toSet.

@[deprecated SetSemiring.toSet_ssubset_toSet (since := "2026-10-13")]

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

Alias of SetSemiring.toSet_ssubset_toSet.

@[deprecated SetSemiring.toSet_zero (since := "2026-10-13")]

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

Alias of SetSemiring.toSet_zero.

@[deprecated SetSemiring.ofSet_empty (since := "2026-10-13")]

theorem Set.up_empty {α : Type u_1} : SetSemiring.ofSet ∅ = 0

Alias of SetSemiring.ofSet_empty.

@[deprecated SetSemiring.toSet_add (since := "2026-10-13")]

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

Alias of SetSemiring.toSet_add.

@[deprecated SetSemiring.ofSet_union (since := "2026-10-13")]

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

Alias of SetSemiring.ofSet_union.

@[deprecated SetSemiring.toSet_mul (since := "2026-10-13")]

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

Alias of SetSemiring.toSet_mul.

@[deprecated SetSemiring.ofSet_mul (since := "2026-10-13")]

theorem Set.up_mul {α : Type u_1} [Mul α] (s t : Set α) : SetSemiring.ofSet (s * t) = SetSemiring.ofSet s * SetSemiring.ofSet t

Alias of SetSemiring.ofSet_mul.

@[deprecated SetSemiring.toSet_one (since := "2026-10-13")]

theorem SetSemiring.down_one {α : Type u_1} [One α] : toSet 1 = 1

Alias of SetSemiring.toSet_one.

@[deprecated SetSemiring.ofSet_one (since := "2026-10-13")]

theorem Set.up_one {α : Type u_1} [One α] : SetSemiring.ofSet 1 = 1

Alias of SetSemiring.ofSet_one.

@[deprecated SetSemiring.imageHom_apply (since := "2026-10-13")]

theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (imageHom f) s = ofSet (⇑f '' toSet s)

Alias of SetSemiring.imageHom_apply.

@[deprecated SetSemiring.imageHom_apply (since := "2026-10-13")]

theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (imageHom f) s = ofSet (⇑f '' toSet s)

Alias of SetSemiring.imageHom_apply.

@[deprecated SetSemiring.imageHom_apply (since := "2026-10-13")]

theorem Set.up_image {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (SetSemiring.imageHom f) s = SetSemiring.ofSet (⇑f '' SetSemiring.toSet s)

Alias of SetSemiring.imageHom_apply.