Documentation
PiBaseLean
.
Theorems
.
T37
.
Theorem
Search
return to top
source
Imports
Init
PiBaseLean.Bundled.Basic
PiBaseLean.Properties.P12.Bundled
PiBaseLean.Properties.P13.Bundled
PiBaseLean.Properties.P135.Bundled
Imported by
PiBase
.
Formal
.
T37
source
theorem
PiBase
.
Formal
.
T37
:
P13
⊓
P135
≤
P12