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

source
def SetSemiring (α : Type u_3) :
Type u_3

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

Instances For
    source
    @[implicit_reducible]
    instance instInhabitedSetSemiring (α : Type u_1) :
    Inhabited (SetSemiring α)
    source
    @[implicit_reducible]
    instance instPartialOrderSetSemiring (α : Type u_1) :
    PartialOrder (SetSemiring α)
    source
    @[implicit_reducible]
    instance instOrderBotSetSemiring (α : Type u_1) :
    OrderBot (SetSemiring α)
    source
    def Set.up {α : Type u_1} :
    Set α ≃ SetSemiring α

    The identity function Set α → SetSemiring α.

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

      The identity function SetSemiring α → Set α.

      Instances For
        source
        @[simp]
        theorem SetSemiring.down_up {α : Type u_1} (s : Set α) :
        SetSemiring.down (Set.up s) = s
        source
        @[simp]
        theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) :
        Set.up (SetSemiring.down s) = s
        source
        theorem SetSemiring.up_le_up {α : Type u_1} {s t : Set α} :
        Set.up s ≤ Set.up t ↔ s ⊆ t
        source
        theorem SetSemiring.up_lt_up {α : Type u_1} {s t : Set α} :
        Set.up s < Set.up t ↔ s ⊂ t
        source
        @[simp]
        theorem SetSemiring.down_subset_down {α : Type u_1} {s t : SetSemiring α} :
        SetSemiring.down s ⊆ SetSemiring.down t ↔ s ≤ t
        source
        @[simp]
        theorem SetSemiring.down_ssubset_down {α : Type u_1} {s t : SetSemiring α} :
        SetSemiring.down s ⊂ SetSemiring.down t ↔ s < t
        source
        @[implicit_reducible]
        instance SetSemiring.instZero {α : Type u_1} :
        Zero (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instAdd {α : Type u_1} :
        Add (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instAddCommMonoid {α : Type u_1} :
        AddCommMonoid (SetSemiring α)
        source
        theorem SetSemiring.zero_def {α : Type u_1} :
        0 = Set.up ∅
        source
        @[simp]
        theorem SetSemiring.down_zero {α : Type u_1} :
        SetSemiring.down 0 = ∅
        source
        @[simp]
        theorem Set.up_empty {α : Type u_1} :
        Set.up ∅ = 0
        source
        theorem SetSemiring.add_def {α : Type u_1} (s t : SetSemiring α) :
        s + t = Set.up (SetSemiring.down s ∪ SetSemiring.down t)
        source
        @[simp]
        theorem SetSemiring.down_add {α : Type u_1} (s t : SetSemiring α) :
        SetSemiring.down (s + t) = SetSemiring.down s ∪ SetSemiring.down t
        source
        @[simp]
        theorem Set.up_union {α : Type u_1} (s t : Set α) :
        Set.up (s ∪ t) = Set.up s + Set.up t
        source
        instance SetSemiring.addLeftMono {α : Type u_1} :
        AddLeftMono (SetSemiring α)

        Since addition on SetSemiring is commutative (it is set union), there is no need to also have the instance AddRightMono (SetSemiring α).

        source
        @[implicit_reducible]
        instance SetSemiring.instNonUnitalNonAssocSemiring {α : Type u_1} [Mul α] :
        NonUnitalNonAssocSemiring (SetSemiring α)
        source
        theorem SetSemiring.mul_def {α : Type u_1} [Mul α] (s t : SetSemiring α) :
        s * t = Set.up (SetSemiring.down s * SetSemiring.down t)
        source
        @[simp]
        theorem SetSemiring.down_mul {α : Type u_1} [Mul α] (s t : SetSemiring α) :
        SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t
        source
        @[simp]
        theorem Set.up_mul {α : Type u_1} [Mul α] (s t : Set α) :
        Set.up (s * t) = Set.up s * Set.up t
        source
        instance SetSemiring.instNoZeroDivisors {α : Type u_1} [Mul α] :
        NoZeroDivisors (SetSemiring α)
        source
        instance SetSemiring.mulLeftMono {α : Type u_1} [Mul α] :
        MulLeftMono (SetSemiring α)
        source
        instance SetSemiring.mulRightMono {α : Type u_1} [Mul α] :
        MulRightMono (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instOne {α : Type u_1} [One α] :
        One (SetSemiring α)
        source
        theorem SetSemiring.one_def {α : Type u_1} [One α] :
        1 = Set.up 1
        source
        @[simp]
        theorem SetSemiring.down_one {α : Type u_1} [One α] :
        SetSemiring.down 1 = 1
        source
        @[simp]
        theorem Set.up_one {α : Type u_1} [One α] :
        Set.up 1 = 1
        source
        @[implicit_reducible]
        instance SetSemiring.instMulOneClass {α : Type u_1} [MulOneClass α] :
        MulOneClass (SetSemiring α)
        source
        @[implicit_reducible]
        noncomputable instance SetSemiring.instNonAssocSemiringOfMulOneClass {α : Type u_1} [MulOneClass α] :
        NonAssocSemiring (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instSemigroup {α : Type u_1} [Semigroup α] :
        Semigroup (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instNonUnitalSemiringOfSemigroup {α : Type u_1} [Semigroup α] :
        NonUnitalSemiring (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instCompleteBooleanAlgebra {α : Type u_1} :
        CompleteBooleanAlgebra (SetSemiring α)
        source
        @[implicit_reducible]
        noncomputable instance SetSemiring.instIdemSemiringOfMonoid {α : Type u_1} [Monoid α] :
        IdemSemiring (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
        CommSemigroup (SetSemiring α)
        source
        @[implicit_reducible]
        instance SetSemiring.instNonUnitalCommSemiringOfCommSemigroup {α : Type u_1} [CommSemigroup α] :
        NonUnitalCommSemiring (SetSemiring α)
        source
        @[implicit_reducible]
        noncomputable instance SetSemiring.instCommMonoid {α : Type u_1} [CommMonoid α] :
        CommMonoid (SetSemiring α)
        source
        @[implicit_reducible]
        noncomputable 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
        noncomputable def SetSemiring.singletonMonoidHom {α : Type u_1} [Monoid α] :
        α →* SetSemiring α

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

        Instances For
          source
          noncomputable 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
            theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
            (imageHom f) s = Set.up (⇑f '' SetSemiring.down s)
            source
            @[simp]
            theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
            SetSemiring.down ((imageHom f) s) = ⇑f '' SetSemiring.down s
            source
            @[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)