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 α) :
        SetSemiring.down (Set.up s) = s
        @[simp]
        theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) :
        Set.up (SetSemiring.down s) = s
        theorem SetSemiring.up_le_up {α : Type u_1} {s : Set α} {t : Set α} :
        Set.up s Set.up t s t
        theorem SetSemiring.up_lt_up {α : Type u_1} {s : Set α} {t : Set α} :
        Set.up s < Set.up t s t
        @[simp]
        theorem SetSemiring.down_subset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} :
        SetSemiring.down s SetSemiring.down t s t
        @[simp]
        theorem SetSemiring.down_ssubset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} :
        SetSemiring.down s SetSemiring.down t s < t
        instance SetSemiring.instZero {α : Type u_1} :
        Equations
        • SetSemiring.instZero = { zero := Set.up }
        instance SetSemiring.instAdd {α : Type u_1} :
        Equations
        • SetSemiring.instAdd = { add := fun (s t : SetSemiring α) => Set.up (SetSemiring.down s SetSemiring.down t) }
        Equations
        theorem SetSemiring.zero_def {α : Type u_1} :
        0 = Set.up
        @[simp]
        theorem SetSemiring.down_zero {α : Type u_1} :
        SetSemiring.down 0 =
        @[simp]
        theorem Set.up_empty {α : Type u_1} :
        Set.up = 0
        theorem SetSemiring.add_def {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) :
        s + t = Set.up (SetSemiring.down s SetSemiring.down t)
        @[simp]
        theorem SetSemiring.down_add {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) :
        SetSemiring.down (s + t) = SetSemiring.down s SetSemiring.down t
        @[simp]
        theorem Set.up_union {α : Type u_1} (s : Set α) (t : Set α) :
        Set.up (s t) = Set.up s + Set.up t
        instance SetSemiring.covariantClass_add {α : Type u_1} :
        CovariantClass (SetSemiring α) (SetSemiring α) (fun (x1 x2 : SetSemiring α) => x1 + x2) fun (x1 x2 : SetSemiring α) => x1 x2
        Equations
        • =
        Equations
        theorem SetSemiring.mul_def {α : Type u_1} [Mul α] (s : SetSemiring α) (t : SetSemiring α) :
        s * t = Set.up (SetSemiring.down s * SetSemiring.down t)
        @[simp]
        theorem SetSemiring.down_mul {α : Type u_1} [Mul α] (s : SetSemiring α) (t : SetSemiring α) :
        SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t
        @[simp]
        theorem Set.up_mul {α : Type u_1} [Mul α] (s : Set α) (t : Set α) :
        Set.up (s * t) = Set.up s * Set.up t
        Equations
        • =
        instance SetSemiring.covariantClass_mul_left {α : Type u_1} [Mul α] :
        CovariantClass (SetSemiring α) (SetSemiring α) (fun (x1 x2 : SetSemiring α) => x1 * x2) fun (x1 x2 : SetSemiring α) => x1 x2
        Equations
        • =
        instance SetSemiring.covariantClass_mul_right {α : Type u_1} [Mul α] :
        CovariantClass (SetSemiring α) (SetSemiring α) (Function.swap fun (x1 x2 : SetSemiring α) => x1 * x2) fun (x1 x2 : SetSemiring α) => x1 x2
        Equations
        • =
        instance SetSemiring.instOne {α : Type u_1} [One α] :
        Equations
        • SetSemiring.instOne = { one := Set.up 1 }
        theorem SetSemiring.one_def {α : Type u_1} [One α] :
        1 = Set.up 1
        @[simp]
        theorem SetSemiring.down_one {α : Type u_1} [One α] :
        SetSemiring.down 1 = 1
        @[simp]
        theorem Set.up_one {α : Type u_1} [One α] :
        Set.up 1 = 1
        Equations
        Equations
        Equations
        Equations
        Equations
        Equations
        Equations
        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
        • SetSemiring.imageHom f = { toFun := fun (s : SetSemiring α) => Set.up (f '' SetSemiring.down s), map_one' := , map_mul' := , map_zero' := , map_add' := }
        Instances For
          theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
          (SetSemiring.imageHom f) s = Set.up (f '' SetSemiring.down s)
          @[simp]
          theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
          SetSemiring.down ((SetSemiring.imageHom f) s) = f '' SetSemiring.down s
          @[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)