English
Let p be a predicate on α and for each x with p(x) assign a set s(x) ⊆ β. Then the union of the sets s(x) over all x with p(x) holds is exactly the union of s(⟨x, hx⟩) over all x and proofs hx that p(x) holds.
Русский
Пусть p — предикат на α и для каждого x с p(x) задано множество s(x) ⊆ β. Тогда объединение множеств s(x) по всем x с p(x) точно равно объединению множеств s(⟨x, hx⟩) по всем x и доказательстваhx того, что p(x) истинно.
LaTeX
$$$\\\\bigcup_{x : \\\\{ x \\\\mid p(x) \\\}} s(x) \\\\;=\\\\; \\\\bigcup_{x \\\\in \\\\alpha} \\\\bigcup_{h \\\\in p(x)} s(\\\\langle x, h \\\\rangle) $$$
Lean4
theorem iUnion_subtype (p : α → Prop) (s : { x // p x } → Set β) :
⋃ x : { x // p x }, s x = ⋃ (x) (hx : p x), s ⟨x, hx⟩ :=
iSup_subtype
