mathlib3 documentation

order.upper_lower.hom

upper_set.Ici etc as sup/Sup/inf/Inf-homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define upper_set.Ici_sup_hom etc. These functions are upper_set.Ici and lower_set.Iic bundled as sup_homs, inf_homs, Sup_homs, or Inf_homs.

source
def upper_set.Ici_sup_hom {α : Type u_1} [semilattice_sup α] :
sup_hom α (upper_set α)

upper_set.Ici as a sup_hom.

Equations
source
@[simp]
theorem upper_set.coe_Ici_sup_hom {α : Type u_1} [semilattice_sup α] :
⇑upper_set.Ici_sup_hom = upper_set.Ici
source
@[simp]
theorem upper_set.Ici_sup_hom_apply {α : Type u_1} [semilattice_sup α] (a : α) :
⇑upper_set.Ici_sup_hom a = upper_set.Ici a
source
def upper_set.Ici_Sup_hom {α : Type u_1} [complete_lattice α] :
Sup_hom α (upper_set α)

upper_set.Ici as a Sup_hom.

Equations
source
@[simp]
theorem upper_set.coe_Ici_Sup_hom {α : Type u_1} [complete_lattice α] :
⇑upper_set.Ici_Sup_hom = upper_set.Ici
source
@[simp]
theorem upper_set.Ici_Sup_hom_apply {α : Type u_1} [complete_lattice α] (a : α) :
⇑upper_set.Ici_Sup_hom a = upper_set.Ici a
source
def lower_set.Iic_inf_hom {α : Type u_1} [semilattice_inf α] :
inf_hom α (lower_set α)

lower_set.Iic as an inf_hom.

Equations
source
@[simp]
theorem lower_set.coe_Iic_inf_hom {α : Type u_1} [semilattice_inf α] :
⇑lower_set.Iic_inf_hom = lower_set.Iic
source
@[simp]
theorem lower_set.Iic_inf_hom_apply {α : Type u_1} [semilattice_inf α] (a : α) :
⇑lower_set.Iic_inf_hom a = lower_set.Iic a
source
def lower_set.Iic_Inf_hom {α : Type u_1} [complete_lattice α] :
Inf_hom α (lower_set α)

lower_set.Iic as an Inf_hom.

Equations
source
@[simp]
theorem lower_set.coe_Iic_Inf_hom {α : Type u_1} [complete_lattice α] :
⇑lower_set.Iic_Inf_hom = lower_set.Iic
source
@[simp]
theorem lower_set.Iic_Inf_hom_apply {α : Type u_1} [complete_lattice α] (a : α) :
⇑lower_set.Iic_Inf_hom a = lower_set.Iic a