preimage_iInter₂ — Mathlib

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]

Похожие утверждения