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 α] : ⇑UpperSet.iciSupHom = UpperSet.Ici

@[simp]

theorem UpperSet.iciSupHom_apply {α : Type u_1} [SemilatticeSup α] (a : α) : UpperSet.iciSupHom a = UpperSet.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 α] : ⇑UpperSet.icisSupHom = UpperSet.Ici

@[simp]

theorem UpperSet.icisSupHom_apply {α : Type u_1} [CompleteLattice α] (a : α) : UpperSet.icisSupHom a = UpperSet.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 α] : ⇑LowerSet.iicInfHom = LowerSet.Iic

@[simp]

theorem LowerSet.iicInfHom_apply {α : Type u_1} [SemilatticeInf α] (a : α) : LowerSet.iicInfHom a = LowerSet.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 α] : ⇑LowerSet.iicsInfHom = LowerSet.Iic

@[simp]

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