English
For any function f, family s_{i,j}, we have f^{-1}(⋃ i (⋃ j, s_{i j})) = ⋃ i (⋃ j, f^{-1}(s_{i j})).
Русский
Для любой функции f, семейства s_{i j} выполняется f^{-1}(⋃_{i} ⋃_{j} s_{i j}) = ⋃_{i} ⋃_{j} f^{-1}(s_{i j}).
LaTeX
$$$f^{-1}\Bigl(\bigcup_i \bigcup_j s_{i j}\Bigr) = \bigcup_i \bigcup_j f^{-1}(s_{i j})$$$
Lean4
theorem preimage_iUnion₂ {f : α → β} {s : ∀ i, κ i → Set β} : (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j := by
simp_rw [preimage_iUnion]