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.

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

Equations
    Instances For
      noncomputable instance instInhabitedSetSemiring (α : Type u_3) :
      Equations
        Equations
          def Set.up {α : Type u_1} :

          The identity function Set α → SetSemiring α.

          Equations
            Instances For
              def SetSemiring.down {α : Type u_1} :

              The identity function SetSemiring α → Set α.

              Equations
                Instances For
                  @[simp]
                  theorem SetSemiring.down_up {α : Type u_1} (s : Set α) :
                  @[simp]
                  theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) :
                  theorem SetSemiring.up_le_up {α : Type u_1} {s t : Set α} :
                  theorem SetSemiring.up_lt_up {α : Type u_1} {s t : Set α} :
                  instance SetSemiring.instZero {α : Type u_1} :
                  Equations
                    instance SetSemiring.instAdd {α : Type u_1} :
                    Equations
                      @[simp]
                      @[simp]
                      theorem Set.up_empty {α : Type u_1} :
                      @[simp]
                      theorem Set.up_union {α : Type u_1} (s t : Set α) :
                      @[simp]
                      theorem Set.up_mul {α : Type u_1} [Mul α] (s t : Set α) :
                      Set.up (s * t) = Set.up s * Set.up t
                      instance SetSemiring.instOne {α : Type u_1} [One α] :
                      Equations
                        theorem SetSemiring.one_def {α : Type u_1} [One α] :
                        1 = Set.up 1
                        @[simp]
                        theorem SetSemiring.down_one {α : Type u_1} [One α] :
                        @[simp]
                        theorem Set.up_one {α : Type u_1} [One α] :
                        Set.up 1 = 1
                        noncomputable instance SetSemiring.instIdemSemiringOfMonoid {α : Type u_1} [Monoid α] :
                        Equations
                          noncomputable instance SetSemiring.instCommMonoid {α : Type u_1} [CommMonoid α] :
                          Equations
                            noncomputable def SetSemiring.imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :

                            The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.

                            Equations
                              Instances For
                                theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
                                @[simp]
                                theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
                                @[simp]
                                theorem Set.up_image {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : Set α) :