Commit 2026-03-24 21:53 72027c75

View on Github →

feat(Topology): cardinality of connected components is bounded by cardinality of fiber (#23835) We show that if f : X → Y is an open and closed map to Y and Y is connected, the number of connected components of X is bounded by the cardinality of the fiber of any point. In particular, if Y has finitely many connected components and f finite fibers, also X as finitely many connected components. From Pi1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Pi.lean

added theorem Set.iUnion_cons

added theorem Set.iUnion_fin_add_one_eq_iUnion_castSucc

added theorem Set.iUnion_fin_add_one_eq_iUnion_succ

added theorem Set.iUnion_snoc

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.iUnion_sumElim

Modified Mathlib/Topology/Clopen.lean

added theorem isClopen_inter_of_disjoint_cover_clopen'

Created Mathlib/Topology/Connected/CardComponents.lean

added theorem IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton

added theorem IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton

added theorem IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace

Modified Mathlib/Topology/Connected/Clopen.lean

added theorem ConnectedComponents.discreteTopology_iff

added theorem ConnectedComponents.equivOfIsClopenOfIsConnected_mk

added theorem ConnectedComponents.equivOfIsClopen_mk

added theorem ConnectedComponents.equivOfIsClopen_symm_mk

added theorem ConnectedComponents.exists_fun_isClopen_of_infinite

added theorem ConnectedComponents.isEmpty_iff_isEmpty

added theorem ConnectedComponents.nonempty_iff_nonempty

added theorem IsClopen.connectedComponentIn_eq

added theorem IsClopen.isPreconnected_iff

added theorem IsClopen.not_isPreconnected_iff