preimage_sInter — Mathlib

English

The preimage of an intersection over a family of sets equals the intersection of the preimages over all members.

Русский

Прообраз пересечения всех множеств равен пересечению их прообразов.

LaTeX

$$$f^{-1}\left(\bigcap_{t \in s} t\right) = \bigcap_{t \in s} f^{-1}(t)$$$

Lean4

@[simp]
theorem preimage_sInter {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t := by
  rw [sInter_eq_biInter, preimage_iInter₂]

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