English
Let p be a predicate on ι and f assigns to each i with a witness h : p i an element α. Then the infimum over i with h of f i h equals the infimum over x of the subtype, i.e., the smallest value attained by f on all eligible indices when the second argument is the proof of p i.
Русский
Пусть p — предикат на ι, а f(i, h) задаёт элемент α для каждого i с доверием h: p(i). Тогда инфимум по всем i с доказательством p(i) равен инфимуму по всем элементам подпредельного множества p, т.е. наименьшее значение функции f на всех допустимых парах.
LaTeX
$$$ \\inf_{i: ι} \\inf_{h: p(i)} f(i,h) = \\inf_{x: \\{ i : ι \\mid p(i) \\}} f(x.val, x.property) $$$
Lean4
theorem iInf_subtype' {p : ι → Prop} {f : ∀ i, p i → α} : ⨅ (i) (h : p i), f i h = ⨅ x : Subtype p, f x x.property :=
(@iInf_subtype _ _ _ p fun x => f x.val x.property).symm
