Theorems · Theorem · general topology

IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → IsClosedMap f → ∀ [ConnectedSpace Y] (y : Y), ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

If f : X → Y is an open and closed map and Y is connected, the number of connected components of X is bounded by the cardinality of the fiber of any point.

Defined in

Mathlib.Topology.Connected.CardComponents

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceConnectedSpace