preimage_sUnion — Mathlib

English

The preimage distributes over the sUnion of a family of sets: the preimage of the union equals the union of the preimages.

Русский

Прообраз распадается по объединению: прообраз объединения равен объединению прообразов.

LaTeX

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

Lean4

@[simp]
theorem preimage_sUnion {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t := by
  rw [sUnion_eq_biUnion, preimage_iUnion₂]

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