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.

UpperSet.Ici as a SupHom.

Equations
  • UpperSet.iciSupHom = { toFun := UpperSet.Ici, map_sup' := }
Instances For
    @[simp]
    theorem UpperSet.coe_iciSupHom {α : Type u_1} [SemilatticeSup α] :
    UpperSet.iciSupHom = UpperSet.Ici
    @[simp]
    theorem UpperSet.iciSupHom_apply {α : Type u_1} [SemilatticeSup α] (a : α) :
    UpperSet.iciSupHom a = UpperSet.Ici a

    UpperSet.Ici as a sSupHom.

    Equations
    • UpperSet.icisSupHom = { toFun := UpperSet.Ici, map_sSup' := }
    Instances For
      @[simp]
      theorem UpperSet.coe_icisSupHom {α : Type u_1} [CompleteLattice α] :
      UpperSet.icisSupHom = UpperSet.Ici
      @[simp]
      theorem UpperSet.icisSupHom_apply {α : Type u_1} [CompleteLattice α] (a : α) :
      UpperSet.icisSupHom a = UpperSet.Ici a

      LowerSet.Iic as an InfHom.

      Equations
      • LowerSet.iicInfHom = { toFun := LowerSet.Iic, map_inf' := }
      Instances For
        @[simp]
        theorem LowerSet.coe_iicInfHom {α : Type u_1} [SemilatticeInf α] :
        LowerSet.iicInfHom = LowerSet.Iic
        @[simp]
        theorem LowerSet.iicInfHom_apply {α : Type u_1} [SemilatticeInf α] (a : α) :
        LowerSet.iicInfHom a = LowerSet.Iic a

        LowerSet.Iic as an sInfHom.

        Equations
        • LowerSet.iicsInfHom = { toFun := LowerSet.Iic, map_sInf' := }
        Instances For
          @[simp]
          theorem LowerSet.coe_iicsInfHom {α : Type u_1} [CompleteLattice α] :
          LowerSet.iicsInfHom = LowerSet.Iic
          @[simp]
          theorem LowerSet.iicsInfHom_apply {α : Type u_1} [CompleteLattice α] (a : α) :
          LowerSet.iicsInfHom a = LowerSet.Iic a