Documentation

Mathlib.Order.UpperLower.Hom

UpperSet.Ici etc as Sup/sSup/Inf/sInf-homomorphisms #

In this file we define UpperSet.iciSupHom etc. These functions are UpperSet.Ici and LowerSet.Iic bundled as SupHoms, InfHoms, sSupHoms, or sInfHoms.

source
def UpperSet.iciSupHom {α : Type u_1} [SemilatticeSup α] :
SupHom α (UpperSet α)

UpperSet.Ici as a SupHom.

Instances For
    source
    @[simp]
    theorem UpperSet.coe_iciSupHom {α : Type u_1} [SemilatticeSup α] :
    ↑UpperSet.iciSupHom = UpperSet.Ici
    source
    @[simp]
    theorem UpperSet.iciSupHom_apply {α : Type u_1} [SemilatticeSup α] (a : α) :
    ↑UpperSet.iciSupHom a = UpperSet.Ici a
    source
    def UpperSet.icisSupHom {α : Type u_1} [CompleteLattice α] :
    sSupHom α (UpperSet α)

    UpperSet.Ici as a sSupHom.

    Instances For
      source
      @[simp]
      theorem UpperSet.coe_icisSupHom {α : Type u_1} [CompleteLattice α] :
      ↑UpperSet.icisSupHom = UpperSet.Ici
      source
      @[simp]
      theorem UpperSet.icisSupHom_apply {α : Type u_1} [CompleteLattice α] (a : α) :
      ↑UpperSet.icisSupHom a = UpperSet.Ici a
      source
      def LowerSet.iicInfHom {α : Type u_1} [SemilatticeInf α] :
      InfHom α (LowerSet α)

      LowerSet.Iic as an InfHom.

      Instances For
        source
        @[simp]
        theorem LowerSet.coe_iicInfHom {α : Type u_1} [SemilatticeInf α] :
        ↑LowerSet.iicInfHom = LowerSet.Iic
        source
        @[simp]
        theorem LowerSet.iicInfHom_apply {α : Type u_1} [SemilatticeInf α] (a : α) :
        ↑LowerSet.iicInfHom a = LowerSet.Iic a
        source
        def LowerSet.iicsInfHom {α : Type u_1} [CompleteLattice α] :
        sInfHom α (LowerSet α)

        LowerSet.Iic as an sInfHom.

        Instances For
          source
          @[simp]
          theorem LowerSet.coe_iicsInfHom {α : Type u_1} [CompleteLattice α] :
          ↑LowerSet.iicsInfHom = LowerSet.Iic
          source
          @[simp]
          theorem LowerSet.iicsInfHom_apply {α : Type u_1} [CompleteLattice α] (a : α) :
          ↑LowerSet.iicsInfHom a = LowerSet.Iic a