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 union over all x in Exists p of f(x) equals the iterated union over i and over all proofs h: p i of f⟨i,h⟩: ⋃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
$$$$\\bigcup_x f(x) = \\bigcup_i \\bigcup_{h: p(i)} f(i,h)$$$$
Lean4
@[simp]
theorem iUnion_exists {p : ι → Prop} {f : Exists p → Set α} : ⋃ x, f x = ⋃ (i) (h : p i), f ⟨i, h⟩ :=
iSup_exists
