connectedComponents_preimage_singleton

English

The preimage of the singleton {mk(x)} under mk is the connected component of x.

Русский

Предобраз меньшого множества {mk(x)} под mk равен связной компоненте x.

LaTeX

$$mk^{-1}({mk(x)}) = \operatorname{connectedComponent}(x)$$

Lean4

/-- The preimage of a singleton in `connectedComponents` is the connected component
of an element in the equivalence class. -/
theorem connectedComponents_preimage_singleton {x : α} :
    (↑) ⁻¹' ({↑x} : Set (ConnectedComponents α)) = connectedComponent x :=
  by
  ext y
  rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']

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