Documentation
PiBaseLean
.
Theorems
.
T78
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
PiBaseLean.Properties.P36.Bundled
PiBaseLean.Properties.P44.Bundled
Imported by
PiBase
.
instBiconnectedSpaceOfPreconnectedSpace
PiBase
.
Formal
.
T78
source
theorem
PiBase
.
instBiconnectedSpaceOfPreconnectedSpace
{
X
:
Type
u_1}
[
TopologicalSpace
X
]
[
BiconnectedSpace
X
]
:
PreconnectedSpace
X
source
theorem
PiBase
.
Formal
.
T78
:
P44
≤
P36