English
There is a bounded lattice hom from a subtype to β given a predicate P on β, mapping each element to its underlying β-value.
Русский
Существует ограниченный гомоморфизм от подтипа к β, заданный предикатом P на β, отображающий элемент в соответствующее значение β.
LaTeX
$$$\\mathrm{subtypeVal} : \\mathrm{BoundedLatticeHom}(\\{x:\\beta\\mid P\\;x\\},\\beta)$$$
Lean4
/-- `Subtype.val` as a `BoundedLatticeHom`. -/
def subtypeVal {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
(Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
letI := Subtype.lattice Psup Pinf
letI := Subtype.boundedOrder Pbot Ptop
BoundedLatticeHom { x : β // P x } β :=
letI := Subtype.lattice Psup Pinf
letI := Subtype.boundedOrder Pbot Ptop
.mk (.subtypeVal Psup Pinf) (by simp [Subtype.coe_top Ptop]) (by simp [Subtype.coe_bot Pbot])
