Structures · Topology
ConnectedSpace
A connected space is a nonempty one where there is no non-trivial open partition.
- Defined in
- Mathlib.Topology.Connected.Basic
- Shape
- One type argument · adds toNonempty
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every ConnectedSpace is also a
Concrete types that are instances6
- TopCat.carrier
- TopologicalSpace.NonemptyCompacts
- OnePoint
- Prod
- Set.Elem
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- isConnected_univ
- isConnected_range
- PathConnectedSpace.of_locallyPathConnectedSpace
- ContinuousMap.sigmaCodHomeomorph
- AnalyticOnNhd.eq_of_frequently_eq
- Function.Surjective.connectedSpace
- AlgebraicGeometry.GeometricallyConnected.connectedSpace
- AnalyticOnNhd.preimage_zero_mem_codiscrete
- IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
- IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton
- TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace
- Continuous.exists_lift_sigma
- Quotient.instConnectedSpace
- ContinuousMap.sigmaCodHomeomorph_symm_apply
- instConnectedSpaceForall
- TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply
- instConnectedSpaceProd
- ConnectedSpace.toPreconnectedSpace
- TopologicalSpace.NonemptyCompacts.instConnectedSpace
- PathConnectedSpace.of_locPathConnectedSpace
- AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen_1
- ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space
- ConnectedSpace.toNonempty
- ContinuousMap.exists_lift_sigma
- instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial
- AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen