biUnion_preimage_singleton — Mathlib

English

The union over y in a set s of the preimage of the singleton {y} equals the preimage of s.

Русский

Объединение по y из s прообраз минимального множества {y} равно прообразу самого множества s.

LaTeX

$$$\bigcup_{y \in s} f^{-1} \{y\} = f^{-1}(s)$$$

Lean4

@[simp]
theorem biUnion_preimage_singleton (f : α → β) (s : Set β) : ⋃ y ∈ s, f ⁻¹' { y } = f ⁻¹' s := by
  rw [← preimage_iUnion₂, biUnion_of_singleton]

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