Structures · Topology
PathConnectedSpace
A topological space is path-connected if it is non-empty and every two points can be joined by a continuous path.
- Defined in
- Mathlib.Topology.Connected.PathConnected
- Shape
- One type argument · adds nonempty, joined
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- Real
- TopCat.carrier
- Units
- AddCircle
- Circle
- TangentSpace
- EuclideanHalfSpace
- EuclideanQuadrant
- Prod
- Set.Elem
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- PathConnectedSpace.somePath
- IsLocalHomeomorph.existsUnique_continuousMap_lifts
- isPathConnected_univ
- PathConnectedSpace.joined
- IsQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective
- PathConnectedSpace.nonempty
- isPathConnected_range
- PathConnectedSpace.exists_path_through_family'
- TopCat.instIsConnectedObjSSetToSSetOfPathConnectedSpaceCarrier
- PathConnectedSpace.somePath.congr_simp
- IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective
- Function.Surjective.pathConnectedSpace
- FundamentalGroup.fundamentalGroupMulEquivOfPathConnected
- Pi.locallyPathConnectedSpace
- TopCat.instIsIsoSingularHomology₀εOfPathConnectedSpaceCarrier
- Pi.instPathConnectedSpace
- Prod.instPathConnectedSpace
- Quotient.instPathConnectedSpace
- IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le
- PathConnectedSpace.exists_path_through_family
- PathConnectedSpace.connectedSpace
- PathConnectedSpace.instSubsingletonZerothHomotopy
Ancestors0
No ancestors.