Documentation
PiBaseLean
.
Theorems
.
T267
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
Mathlib.Topology.Separation.AlexandrovDiscrete
PiBaseLean.Properties.P2.Bundled
PiBaseLean.Properties.P52.Bundled
PiBaseLean.Properties.P90.Bundled
Imported by
PiBase
.
Formal
.
T267
source
theorem
PiBase
.
Formal
.
T267
:
P90
⊓
P2
≤
P52
Theorem T267: P90 (AlexandrovDiscrete) + P2 (T1Space) => P52 (DiscreteTopology)