Documentation

PiBaseLean.Theorems.T583.Theorem

source
instance PiBase.PresimplyConnectedSpaceOfLocallySimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] :
PresimplyConnectedSpace X
source
theorem PiBase.Formal.T583 :
P199 ≤ P200