Theorem IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton

Modification history

2026-03-24 21:53
Mathlib/Topology/Connected/CardComponents.lean
feat(Topology): cardinality of connected components is bounded by cardinality of fiber (#23835) …
Added IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singletonView on Github →