English
Let p be a predicate on ι and f a function assigning a set to each witness ⟨i, h⟩ with h a proof of p i. Then the intersection over all x in Exists p of f(x) equals the iterated intersection over i of the intersections over all proofs h that p i holds: ⋂x f(x) = ⋂i (⋂h: p i, f⟨i,h⟩).
Русский
Пусть p — предикат на ι, а f — отображение, ставящее множество для каждого свидетеля ⟨i, h⟩ с доказательством p i. Тогда пересечение по всем x из Exists p множеств f(x) равно итерационному пересечению по i и по всем доказательствам h того, что p i выполняется: ⋂x f(x) = ⋂i (⋂h: p i, f⟨i,h⟩).
LaTeX
$$$$\\bigcap_x f(x) = \\bigcap_{i} \\bigcap_{h: p(i)} f(i,h)$$$$
Lean4
@[simp]
theorem iInter_exists {p : ι → Prop} {f : Exists p → Set α} : ⋂ x, f x = ⋂ (i) (h : p i), f ⟨i, h⟩ :=
iInf_exists
