Description: The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hbtlem.p | |
|
hbtlem.u | |
||
hbtlem.s | |
||
hbtlem3.r | |
||
hbtlem3.i | |
||
hbtlem3.j | |
||
hbtlem3.ij | |
||
hbtlem5.e | |
||
Assertion | hbtlem5 | |