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.

Equations

• UpperSet.iciSupHom = { toFun := UpperSet.Ici, map_sup' := ⋯ }

@[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.

Equations

• UpperSet.icisSupHom = { toFun := UpperSet.Ici, map_sSup' := ⋯ }

@[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.

Equations

• LowerSet.iicInfHom = { toFun := LowerSet.Iic, map_inf' := ⋯ }

@[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.

Equations

• LowerSet.iicsInfHom = { toFun := LowerSet.Iic, map_sInf' := ⋯ }

@[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