Documentation
PiBaseLean
.
Theorems
.
T45
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
PiBaseLean.Properties.P3.Bundled
PiBaseLean.Properties.P48.Bundled
PiBaseLean.Properties.P49.Bundled
Imported by
PiBase
.
Formal
.
T45
source
theorem
PiBase
.
Formal
.
T45
:
P49
⊓
P3
≤
P48