English
If P is a predicate on α closed under inf and top, then infimum over a Finset t of β with values in the subtype {x ∈ α | P x} corresponds to the infimum in α of the underlying values.
Русский
Если предикат P над α замкнут по инф и содержит верхний элемент, то инфимум по t из значений в подтипе {x | P x} соответствует инфимуму по α от соответствующих значений.
LaTeX
$$$ \\text{theorem inf_coe ... } \\left( t, f \\right) : \\ (\\inf_{x\\in t} f(x)) = \\inf_{x\\in t} (f(x))^{\\uparrow} $$$
Lean4
/-- Computing `inf` in a subtype (closed under `inf`) is the same as computing it in `α`. -/
theorem inf_coe {P : α → Prop} {Ptop : P ⊤} {Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)} (t : Finset β)
(f : β → { x : α // P x }) :
(@inf { x // P x } _ (Subtype.semilatticeInf Pinf) (Subtype.orderTop Ptop) t f : α) = t.inf fun x => ↑(f x) :=
@sup_coe αᵒᵈ _ _ _ _ Ptop Pinf t f
