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.

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

UpperSet.Ici as a SupHom.

@[simp]

theorem UpperSet.coe_iciSupHom {α : Type u_1} [SemilatticeSup α] : ⇑iciSupHom = Ici

@[simp]

theorem UpperSet.iciSupHom_apply {α : Type u_1} [SemilatticeSup α] (a : α) : iciSupHom a = Ici a

def UpperSet.icisSupHom {α : Type u_1} [CompleteLattice α] : sSupHom α (UpperSet α)

UpperSet.Ici as a sSupHom.

@[simp]

theorem UpperSet.coe_icisSupHom {α : Type u_1} [CompleteLattice α] : ⇑icisSupHom = Ici

@[simp]

theorem UpperSet.icisSupHom_apply {α : Type u_1} [CompleteLattice α] (a : α) : icisSupHom a = Ici a

def LowerSet.iicInfHom {α : Type u_1} [SemilatticeInf α] : InfHom α (LowerSet α)

LowerSet.Iic as an InfHom.

@[simp]

theorem LowerSet.coe_iicInfHom {α : Type u_1} [SemilatticeInf α] : ⇑iicInfHom = Iic

@[simp]

theorem LowerSet.iicInfHom_apply {α : Type u_1} [SemilatticeInf α] (a : α) : iicInfHom a = Iic a

def LowerSet.iicsInfHom {α : Type u_1} [CompleteLattice α] : sInfHom α (LowerSet α)

LowerSet.Iic as an sInfHom.

@[simp]

theorem LowerSet.coe_iicsInfHom {α : Type u_1} [CompleteLattice α] : ⇑iicsInfHom = Iic

@[simp]

theorem LowerSet.iicsInfHom_apply {α : Type u_1} [CompleteLattice α] (a : α) : iicsInfHom a = Iic a