English
If x,y belong to the subtype { z : α | P z } and α has a semilatticeInf, then the infimum in the subtype projects to the infimum in α.
Русский
Пусть x,y принадлежат подтипy { z : α | P z } и в α есть полупреступка; тогда инфимум в подтипе проецируется на инфимум в α.
LaTeX
$$$[SemilatticeInf\\;\\alpha] \\, {P:\\alpha\\to\\mathrm{Prop}} \\, (Pinf:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcap y)) \\, (x\\;y:\\text{Subtype } P) \\Rightarrow ((x\\sqcap y : \\text{Subtype } P)\\uparrow)=(x\\uparrow\\sqcap y\\uparrow)$$$
Lean4
@[simp, norm_cast]
theorem coe_inf [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) (x y : Subtype P) :
(haveI := Subtype.semilatticeInf Pinf;
(x ⊓ y : Subtype P) :
α) =
(x ⊓ y : α) :=
rfl
