English
The union over h : p of s h equals the dependent conditional s h if p; otherwise it is empty.
Русский
Объединение по h : p множества s(h) равно зависимому условному множеству s(h) при p; иначе пустое множество.
LaTeX
$$$\\bigcup_{h : p} s(h) = \\begin{cases} s(h), & h : p \\\\ \\\\emptyset, & \\text{ otherwise} \\end{cases}$$$
Lean4
theorem iUnion_eq_dif {p : Prop} [Decidable p] (s : p → Set α) : ⋃ h : p, s h = if h : p then s h else ∅ :=
iSup_eq_dif _