English
Let x be an element of the union over i of the unions over j of s(i, j). Then there exist indices i and j with x ∈ s(i, j).
Русский
Пусть x принадлежит объединению по i затем по j множеств s(i, j). Тогда существуют индексы i и j такие, что x ∈ s(i, j).
LaTeX
$$$x \\\\in \\\\bigcup_i \\\\bigcup_j s(i,j) \iff \\\\exists i \\\\exists j, x \\\\in s(i,j)$$$
Lean4
theorem mem_iUnion₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋃ (i) (j), s i j) ↔ ∃ i j, x ∈ s i j := by
simp_rw [mem_iUnion]