image_eq_of_connectedComponent_eq

English

Let f: α → β be continuous, where β is totally disconnected. If a and b lie in the same connected component of α, then f(a) = f(b). In other words, f is constant on each connected component of α.

Русский

Пусть f: α → β непрерывно, причем β — полностью раздельное пространство. Если точки a и b принадлежат одной связной компоненте пространства α, то f(a) = f(b). Иными словами, отображение f константно на каждой связной компоненте α.

LaTeX

$$$\\forall a,b \in \alpha\, (\\operatorname{connectedComponent}(a) = \\operatorname{connectedComponent}(b) \\Rightarrow f(a) = f(b))$$$

Lean4

theorem image_eq_of_connectedComponent_eq (h : Continuous f) (a b : α)
    (hab : connectedComponent a = connectedComponent b) : f a = f b :=
  singleton_eq_singleton_iff.1 <|
    h.image_connectedComponent_eq_singleton a ▸ h.image_connectedComponent_eq_singleton b ▸ hab ▸ rfl

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