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' := (_ : ∀ (a b : α), UpperSet.Ici (a ⊔ b) = UpperSet.Ici a ⊔ UpperSet.Ici b) }

@[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' := (_ : ∀ (s : Set α), UpperSet.Ici (sSup s) = sSup (UpperSet.Ici '' s)) }

@[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' := (_ : ∀ (a b : α), LowerSet.Iic (a ⊓ b) = LowerSet.Iic a ⊓ LowerSet.Iic b) }

@[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' := (_ : ∀ (s : Set α), LowerSet.Iic (sInf s) = sInf (LowerSet.Iic '' s)) }

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