English
The join of two elements of a predicate-lifted type is computed by taking the join of the underlying α-values and proving membership via Psup.
Русский
Слияние двух элементов подтипа через конструктор mkSup mk выполняется по Join исходных значений и доказательству приналежности.
LaTeX
$$$[SemilatticeSup\\alpha] \\{P:\\alpha\\to\\mathrm{Prop}\\} \\; (Psup:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcup y)) \\; {x\\;y:\\alpha}\\; (hx:P x) (hy:P y) : (\\langle x,hx\\rangle \\lor \\langle y,hy\\rangle) = \\langle x\\lor y, Psup hx hy\\rangle$$$
Lean4
@[simp]
theorem mk_sup_mk [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) {x y : α} (hx : P x)
(hy : P y) :
(haveI := Subtype.semilatticeSup Psup;
(⟨x, hx⟩ ⊔ ⟨y, hy⟩ : Subtype P)) =
⟨x ⊔ y, Psup hx hy⟩ :=
rfl
