Documentation
PiBaseLean
.
Theorems
.
T268
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
Mathlib.Topology.GDelta.MetrizableSpace
PiBaseLean.Properties.P121.Bundled
PiBaseLean.Properties.P15.Bundled
Imported by
PiBase
.
Formal
.
T268
source
theorem
PiBase
.
Formal
.
T268
:
P121
≤
P15