connectedComponents_preimage_image

English

For any set U, the preimage of the image of U equals the union of connected components of elements of U.

Русский

Для любого множества U предобраз образа U равен объединению связных компонент элементов U.

LaTeX

$$preimage\mk( image\mk(U)) = \bigcup_{x\in U} \operatorname{connectedComponent}(x)$$

Lean4

/-- The preimage of the image of a set under the quotient map to `connectedComponents α`
is the union of the connected components of the elements in it. -/
theorem connectedComponents_preimage_image (U : Set α) :
    (↑) ⁻¹' ((↑) '' U : Set (ConnectedComponents α)) = ⋃ x ∈ U, connectedComponent x := by
  simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion]

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