Documentation
PiBaseLean
.
Theorems
.
T284
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
PiBaseLean.Properties.P23.Bundled
PiBaseLean.Properties.P90.Bundled
Imported by
PiBase
.
Formal
.
T284
source
theorem
PiBase
.
Formal
.
T284
:
P90
≤
P23
Theorem T284: P90 (AlexandrovDiscrete) => P23 (WeaklyLocallyCompactSpace)