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 SupHom
s, InfHom
s, sSupHom
s, or sInfHom
s.
UpperSet.Ici
as a SupHom
.
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
.
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
.
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
.
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