English
If x,y are elements of the subtype { z : α | P z } and α has a semilatticeSup, then the supremum computed inside the subtype projects to the supremum in α.
Русский
Пусть x,y — элементы подтипа { z : α | P z } и в α есть полурешетка верх; тогда супремум внутри подтипа проецируется на супремум в α.
LaTeX
$$$[SemilatticeSup\\;\\alpha] \\, {P:\\alpha\\to\\mathrm{Prop}} \\, (Psup:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcup y)) \\, (x\\;y:\\text{Subtype } P) \Rightarrow ((x\\sqcup y : \\text{Subtype } P)\\uparrow)=(x\\uparrow\\sqcup y\\uparrow)$$$
Lean4
@[simp, norm_cast]
theorem coe_sup [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (x y : Subtype P) :
(haveI := Subtype.semilatticeSup Psup;
(x ⊔ y : Subtype P) :
α) =
(x ⊔ y : α) :=
rfl
