Structures · Topology
LocallyPathConnectedSpace
A topological space is locally path connected if, at every point, path connected neighborhoods form a neighborhood basis.
- Shape
- One type argument · adds path_connected_basis
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances9
- UpperHalfPlane
- EuclideanHalfSpace
- EuclideanQuadrant
- Subtype
- Prod
- Sum
- Sigma
- Quotient
- Quot
How is a type an instance?
Loading the hierarchy index…
Assumed by58
- IsOpen.pathComponentIn
- LocallyPathConnectedSpace.path_connected_basis
- IsOpen.locallyPathConnectedSpace
- connectedComponentsEquivZerothHomotopy
- Topology.IsOpenEmbedding.locallyPathConnectedSpace
- IsLocalHomeomorph.existsUnique_continuousMap_lifts
- IsClopen.pathComponent
- pathComponentIn_mem_nhds
- Topology.IsQuotientMap.locallyPathConnectedSpace
- pathComponent_eq_connectedComponent
- IsOpen.pathComponent
- LocallyPathConnectedSpace.coinduced
- PathConnectedSpace.of_locallyPathConnectedSpace
- IsCoveringMapOn.existsUnique_continuousMap_lifts
- Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace
- Complex.exists_continuousOn_eqOn_exp_comp
- IsClosed.pathComponent
- pathConnectedSpace_iff_connectedSpace
- IsCoveringMap.existsUnique_continuousMap_lifts
- ChartedSpace.locallyPathConnectedSpace
- OpenNormalAddSubgroup.pathComponentZero
- OpenNormalSubgroup.pathComponentOne
- Complex.exists_continuousOn_pow_eq
- connectedComponent_eq_iff_joined
- pathConnected_subset_basis
- Sum.locPathConnectedSpace
- Prod.locallyPathConnectedSpace
- coe_connectedComponentsEquivZerothHomotopy_symm
- OpenNormalSubgroup.pathComponentOne_carrier
- Quotient.locPathConnectedSpace
- IsOpen.locPathConnectedSpace
- LocPathConnectedSpace.path_connected_basis
- Quot.locallyPathConnectedSpace
- Complex.UnitDisc.exists_continuousOn_pow_eq
- Sum.locallyPathConnectedSpace
- OpenNormalAddSubgroup.pathComponentZero_carrier
- connectedComponentsEquivZerothHomotopy_symm_apply
- LocPathConnectedSpace.coinduced
- OpenNormalAddSubgroup.instIsClosedCoePathComponentZero
- Topology.IsOpenEmbedding.locPathConnectedSpace
- PathConnectedSpace.of_locPathConnectedSpace
- Pi.locallyPathConnectedSpace
- OpenNormalSubgroup.instIsClosedCoePathComponentOne
- IsOpen.isConnected_iff_isPathConnected
- Sigma.locallyPathConnectedSpace
- Quotient.locallyPathConnectedSpace
- isOpen_isPathConnected_basis
- IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le
- Quot.locPathConnectedSpace
- connectedComponentsEquivZerothHomotopy_apply
Ancestors0
No ancestors.