English
Let p : ι → Prop, q : ι → ι' → Prop, and s : ∀ x y, p x ∧ q x y → Set α. Then the union of the sets s(x,y,h) over all x, y and h with h ∈ p x ∧ q x y equals the union over x, hx ∈ p x and y, hy ∈ q x y of s(x,y,⟨hx,hy⟩).
Русский
Пусть p : ι → Prop, q : ι → ι' → Prop и s : ∀ x y, p x ∧ q x y → Set α. Тогда объединение множеств s(x,y,h) по всем x, y и h с условием h ∈ p x ∧ q x y равно объединению по всем x, hx ∈ p x и y, hy ∈ q x y настойчивному индексу i.e. s(x,y,⟨hx,hy⟩).
LaTeX
$$$$\\bigcup_{x:\\iota} \\bigcup_{y:\\iota'} \\bigcup_{h: p(x) \\land q(x,y)} s(x,y,h) = \\bigcup_{x:\\iota} \\bigcup_{hx: p(x)} \\bigcup_{y:\\iota'} \\bigcup_{hy: q(x,y)} s(x,y,\\langle hx, hy\\rangle).$$$$
Lean4
@[simp]
theorem biUnion_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋃ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩ := by
simp only [iUnion_and, @iUnion_comm _ ι']
