Theorems · Theorem · general topology

Continuous.image_connectedComponent_eq_singleton

∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [TotallyDisconnectedSpace β]
  {f : α → β}, Continuous f → ∀ (a : α), f '' connectedComponent a = {f a}

The image of a connected component in a totally disconnected space is a singleton.

Defined in

Mathlib.Topology.Connected.TotallyDisconnected

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpace