Documentation
LeanPool
.
OneManifold
.
OneMfld
.
LocallyConnected
Search
return to top
source
Imports
Init
Mathlib.Tactic.FunProp
Mathlib.Tactic.Linarith
Mathlib.Tactic.ReduceModChar
Mathlib.Tactic.Ring
Mathlib.Analysis.Convex.PathConnected
Mathlib.Topology.Bornology.Real
Mathlib.Topology.UniformSpace.Real
Mathlib.Topology.Instances.NNReal.Lemmas
Imported by
OneMfld
.
instLocallyConnectedSpaceNNReal_leanPool
LocallyConnected
#
Supporting results for the classification of compact one-dimensional manifolds.
source
instance
OneMfld
.
instLocallyConnectedSpaceNNReal_leanPool
:
LocallyConnectedSpace
NNReal