Theorems · Theorem · general topology

IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f →
    IsClosedMap f →
      ∀ [Finite (ConnectedComponents Y)],
        Continuous f → (∀ (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.

Defined in

Mathlib.Topology.Connected.CardComponents

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceFinite