Theorems · Theorem · general topology

Continuous.image_eq_of_connectedComponent_eq

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

Defined in

Mathlib.Topology.Connected.TotallyDisconnected

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpace