English
The meet of two elements of { z : α | P z } is given by the meet of their underlying values, with a proof that the result lies in the subtype.
Русский
Объединение двух элементов подтипа через конструктор mkInf mk задается через инфумум базовых значений и доказательство принадлежности.
LaTeX
$$$[SemilatticeInf\\alpha] \\{P:\\alpha\\to\\mathrm{Prop}\\} (Pinf:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcap y)) \\; {x\\;y:\\alpha}\\; (hx:P x) (hy:P y) : ((\\langle x,hx\\rangle \\sqcap \\langle y,hy\\rangle) = \\langle x\\sqcap y, Pinf hx hy\\rangle)$$$
Lean4
@[simp]
theorem mk_inf_mk [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) {x y : α} (hx : P x)
(hy : P y) :
(haveI := Subtype.semilatticeInf Pinf;
(⟨x, hx⟩ ⊓ ⟨y, hy⟩ : Subtype P)) =
⟨x ⊓ y, Pinf hx hy⟩ :=
rfl
