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

source
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".

Instances For
    source
    @[instance_reducible]
    instance instInhabitedSetSemiring (α : Type u_1) :
    Inhabited (SetSemiring α)
    source
    @[instance_reducible]
    instance instCompleteAtomicBooleanAlgebraSetSemiring (α : Type u_1) :
    CompleteAtomicBooleanAlgebra (SetSemiring α)
    source
    def SetSemiring.ofSet {α : Type u_1} :
    Set α ≃ SetSemiring α

    The identity equivalence between Set α and SetSemiring α.

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

      The identity equivalence between SetSemiring α and Set α.

      Instances For
        source
        @[simp]
        theorem SetSemiring.toSet_ofSet {α : Type u_1} (s : Set α) :
        toSet (ofSet s) = s
        source
        @[simp]
        theorem SetSemiring.ofSet_toSet {α : Type u_1} (s : SetSemiring α) :
        ofSet (toSet s) = s
        source
        @[simp]
        theorem SetSemiring.ofSet_le_ofSet {α : Type u_1} {s t : Set α} :
        ofSet s ≤ ofSet t ↔ s ⊆ t
        source
        @[simp]
        theorem SetSemiring.ofSet_lt_ofSet {α : Type u_1} {s t : Set α} :
        ofSet s < ofSet t ↔ s ⊂ t
        source
        @[simp]
        theorem SetSemiring.toSet_subset_toSet {α : Type u_1} {s t : SetSemiring α} :
        toSet s ⊆ toSet t ↔ s ≤ t
        source
        @[simp]
        theorem SetSemiring.toSet_ssubset_toSet {α : Type u_1} {s t : SetSemiring α} :
        toSet s ⊂ toSet t ↔ s < t
        source
        @[simp]
        theorem SetSemiring.symm_toSet {α : Type u_1} :
        toSet.symm = ofSet
        source
        @[simp]
        theorem SetSemiring.symm_ofSet {α : Type u_1} :
        ofSet.symm = toSet
        source
        @[instance_reducible]
        instance SetSemiring.instZero {α : Type u_1} :
        Zero (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instAdd {α : Type u_1} :
        Add (SetSemiring α)
        source
        theorem SetSemiring.zero_def {α : Type u_1} :
        0 = ofSet ∅
        source
        @[simp]
        theorem SetSemiring.toSet_zero {α : Type u_1} :
        toSet 0 = ∅
        source
        @[simp]
        theorem SetSemiring.ofSet_empty {α : Type u_1} :
        ofSet ∅ = 0
        source
        theorem SetSemiring.add_def {α : Type u_1} (s t : SetSemiring α) :
        s + t = ofSet (toSet s ∪ toSet t)
        source
        @[simp]
        theorem SetSemiring.toSet_add {α : Type u_1} (s t : SetSemiring α) :
        toSet (s + t) = toSet s ∪ toSet t
        source
        @[simp]
        theorem SetSemiring.ofSet_union {α : Type u_1} (s t : Set α) :
        ofSet (s ∪ t) = ofSet s + ofSet t
        source
        @[instance_reducible]
        instance SetSemiring.instAddCommMonoid {α : Type u_1} :
        AddCommMonoid (SetSemiring α)
        source
        instance SetSemiring.instAddLeftMono {α : Type u_1} :
        AddLeftMono (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instNonUnitalNonAssocSemiring {α : Type u_1} [Mul α] :
        NonUnitalNonAssocSemiring (SetSemiring α)
        source
        theorem SetSemiring.mul_def {α : Type u_1} [Mul α] (s t : SetSemiring α) :
        s * t = ofSet (toSet s * toSet t)
        source
        @[simp]
        theorem SetSemiring.toSet_mul {α : Type u_1} [Mul α] (s t : SetSemiring α) :
        toSet (s * t) = toSet s * toSet t
        source
        @[simp]
        theorem SetSemiring.ofSet_mul {α : Type u_1} [Mul α] (s t : Set α) :
        ofSet (s * t) = ofSet s * ofSet t
        source
        instance SetSemiring.instNoZeroDivisors {α : Type u_1} [Mul α] :
        NoZeroDivisors (SetSemiring α)
        source
        instance SetSemiring.instMulLeftMono {α : Type u_1} [Mul α] :
        MulLeftMono (SetSemiring α)
        source
        instance SetSemiring.instMulRightMono {α : Type u_1} [Mul α] :
        MulRightMono (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instOne {α : Type u_1} [One α] :
        One (SetSemiring α)
        source
        theorem SetSemiring.one_def {α : Type u_1} [One α] :
        1 = ofSet 1
        source
        @[simp]
        theorem SetSemiring.toSet_one {α : Type u_1} [One α] :
        toSet 1 = 1
        source
        @[simp]
        theorem SetSemiring.ofSet_one {α : Type u_1} [One α] :
        ofSet 1 = 1
        source
        @[instance_reducible]
        instance SetSemiring.instMulOneClass {α : Type u_1} [MulOneClass α] :
        MulOneClass (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instNonAssocSemiringOfMulOneClass {α : Type u_1} [MulOneClass α] :
        NonAssocSemiring (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instSemigroup {α : Type u_1} [Semigroup α] :
        Semigroup (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instNonUnitalSemiringOfSemigroup {α : Type u_1} [Semigroup α] :
        NonUnitalSemiring (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instIdemSemiringOfMonoid {α : Type u_1} [Monoid α] :
        IdemSemiring (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
        CommSemigroup (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instNonUnitalCommSemiringOfCommSemigroup {α : Type u_1} [CommSemigroup α] :
        NonUnitalCommSemiring (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instCommMonoid {α : Type u_1} [CommMonoid α] :
        CommMonoid (SetSemiring α)
        source
        @[instance_reducible]
        instance SetSemiring.instIdemCommSemiringOfCommMonoid {α : Type u_1} [CommMonoid α] :
        IdemCommSemiring (SetSemiring α)
        source
        instance SetSemiring.instCanonicallyOrderedAdd {α : Type u_1} :
        CanonicallyOrderedAdd (SetSemiring α)
        source
        instance SetSemiring.instIsOrderedRing {α : Type u_1} [CommMonoid α] :
        IsOrderedRing (SetSemiring α)
        source
        def SetSemiring.singletonMonoidHom {α : Type u_1} [Monoid α] :
        α →* SetSemiring α

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

        Instances For
          source
          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.

          Instances For
            source
            @[simp]
            theorem SetSemiring.imageHom_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
            (imageHom f) s = ofSet (⇑f '' toSet s)
            source
            @[simp]
            theorem SetSemiring.imageHom_id {α : Type u_1} [MulOneClass α] :
            imageHom (MonoidHom.id α) = RingHom.id (SetSemiring α)
            source
            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)
            source
            @[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 α.

            Instances For
              source
              @[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 α.

              Instances For
                source
                @[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.

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

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

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

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

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

                source
                @[deprecated SetSemiring.toSet_zero (since := "2026-10-13")]
                theorem SetSemiring.down_zero {α : Type u_1} :
                toSet 0 = ∅

                Alias of SetSemiring.toSet_zero.

                source
                @[deprecated SetSemiring.ofSet_empty (since := "2026-10-13")]
                theorem Set.up_empty {α : Type u_1} :
                SetSemiring.ofSet ∅ = 0

                Alias of SetSemiring.ofSet_empty.

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

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

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

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

                source
                @[deprecated SetSemiring.toSet_one (since := "2026-10-13")]
                theorem SetSemiring.down_one {α : Type u_1} [One α] :
                toSet 1 = 1

                Alias of SetSemiring.toSet_one.

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

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

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

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