Cardinality of connected components under open and closed maps

Let f : X → Y be an open and closed map.

Main results

• IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton: If Y is connected, the number of connected components of X is bounded by the cardinality of the fiber of f at y.
• IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton: If f is also continuous with finite fibers and Y has finitely many connected components, so does X.

theorem IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf₁ : IsOpenMap f) (hf₂ : 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.

theorem IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf₁ : IsOpenMap f) (hf₂ : IsClosedMap f) [ConnectedSpace Y] {y : Y} (hy : (f ⁻¹' {y}).Finite) : Finite (ConnectedComponents X)

theorem IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf₁ : IsOpenMap f) (hf₂ : IsClosedMap f) [Finite (ConnectedComponents Y)] (hfc : Continuous f) (h : ∀ (y : Y), (f ⁻¹' {y}).Finite) : Finite (ConnectedComponents X)

If f : X → Y is continuous, open and closed with finite fibers and Y has finitely many connected components, so does X.