English
Let P be a predicate on β with P top and closure under inf; then InfTopHom from subtype {x ∈ β | P x} to β exists via inclusion.
Русский
Пусть P — предикат на β с P верх и замкнутостью по inf; тогда InfTopHom из подтипа {x ∈ β | P x} в β существует через включение.
LaTeX
$$$\\text{subtypeVal} : \\{x:\\beta\\mid P x\\} \\to \\beta$$$
Lean4
/-- `Subtype.val` as an `InfTopHom`. -/
def subtypeVal {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
letI := Subtype.orderTop Ptop
letI := Subtype.semilatticeInf Pinf
InfTopHom { x : β // P x } β :=
letI := Subtype.orderTop Ptop
letI := Subtype.semilatticeInf Pinf
.mk (InfHom.subtypeVal Pinf) (by simp [Subtype.coe_top Ptop])
