CardComponents

📁 Source: Mathlib/Topology/Connected/CardComponents.lean

Statistics

Metric	Count
Definitions	0
Theorems enatCard_connectedComponents_le_encard_preimage_singleton, finite_connectedComponents_of_finite_preimage_singleton, finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace	3
Total	3

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enatCard_connectedComponents_le_encard_preimage_singleton 📖	mathematical	IsOpenMap IsClosedMap	ENat instLEENat ENat.card ConnectedComponents Set.encard Set.preimage Set Set.instSingletonSet	—	Set.univ_inter Set.iUnion_inter Set.encard_iUnion_of_finite Finite.of_fintype Disjoint.inter_left Disjoint.inter_right Finset.sum_const Fintype.card_fin nsmul_eq_mul mul_one instReflLe finsum_eq_sum_of_fintype Fintype.sum_mono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Set.one_le_encard_iff_nonempty IsClopen.eq_univ ConnectedSpace.toPreconnectedSpace Set.Nonempty.image Set.mem_univ finite_or_infinite nonempty_fintype ENat.card_eq_coe_fintype_card IsClopen.preimage isClopen_discrete Finite.instDiscreteTopology TotallyDisconnectedSpace.t1Space ConnectedComponents.totallyDisconnectedSpace ConnectedComponents.continuous_coe Set.Nonempty.preimage Set.singleton_nonempty ConnectedComponents.surjective_coe Disjoint.preimage EquivLike.toEmbeddingLike Set.iUnion_singleton_eq_range EquivLike.range_eq_univ ENat.card_eq_top_of_infinite ConnectedComponents.exists_fun_isClopen_of_infinite IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd le_trans Nat.cast_add Nat.cast_one
finite_connectedComponents_of_finite_preimage_singleton 📖	mathematical	IsOpenMap IsClosedMap Continuous Set.Finite Set.preimage Set Set.instSingletonSet	Finite ConnectedComponents	—	ConnectedComponents.surjective_coe isConnected_iff_connectedSpace isConnected_connectedComponent connectedComponents_preimage_singleton finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace restrictPreimage IsClosedMap.restrictPreimage mem_connectedComponent Set.finite_image_iff Function.Injective.injOn Subtype.val_injective Set.ext Finite.of_equiv Finite.instSigma IsClopen.preimage isClopen_discrete Finite.instDiscreteTopology TotallyDisconnectedSpace.t1Space ConnectedComponents.totallyDisconnectedSpace Continuous.comp ConnectedComponents.continuous_coe Disjoint.preimage Set.iUnion_eq_univ_iff
finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace 📖	mathematical	IsOpenMap IsClosedMap	Finite ConnectedComponents	—	ENat.card_lt_top lt_of_le_of_lt enatCard_connectedComponents_le_encard_preimage_singleton Set.Finite.encard_lt_top

---

← Back to Index