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