English
Let P be a predicate on β, closed under ⊥ and ⊔ (i.e. P ⊥ holds and P is preserved by join). Then the inclusion of the subtype {x ∈ β | P x} into β is a SupBotHom.
Русский
Пусть P — свойство на β, замкнутое относительно ⊥ и ⊔ (P ⊥ и замкнутость относительно объединения). Тогда включение подмножества {x ∈ β | P x} в β является SupBotHom.
LaTeX
$$$\\text{subtypeVal} : \\{x:\\beta\\mid P x\\} \\to \\beta \\\\text{ (при условии } P\\bot\\text{ и }\\forall x,y(Px\\to Py\\to P(x\\lor y)))$$$
Lean4
/-- `Subtype.val` as a `SupBotHom`. -/
def subtypeVal {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
letI := Subtype.orderBot Pbot
letI := Subtype.semilatticeSup Psup
SupBotHom { x : β // P x } β :=
letI := Subtype.orderBot Pbot
letI := Subtype.semilatticeSup Psup
.mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_bot Pbot])
