English
If you index a two-parameter family of sets by i and j, the preimage distributes over a two-parameter intersection: the preimage of s(i,j) over both indices equals the intersection of the preimages.
Русский
При двухиндексном наборе множеств прообраз распределяется по двойному пересечению.
LaTeX
$$$f^{-1}\left(\bigcap_{i} \bigcap_{j} s_{i j}\right) = \bigcap_i \bigcap_j f^{-1}(s_{i j})$$$
Lean4
theorem preimage_iInter₂ {f : α → β} {s : ∀ i, κ i → Set β} : (f ⁻¹' ⋂ (i) (j), s i j) = ⋂ (i) (j), f ⁻¹' s i j := by
simp_rw [preimage_iInter]