PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
increasing-implies2
n:
, f:(
n
). increasing(f;n)
(
i:
n, j:
i. f(j)
(f(i)))
By:
Auto
THEN
FwdThru
Thm*
k:
, f:(
k
). increasing(f;k)
(
x,y:
k. x < y
f(x) < f(y)) [-3]
THEN
InstHyp [j;i] -1
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
n:
, f:(n
). increasing(f;n) 
(i:n, j:i. f(j) 
(f(i)))
k:, f:(k
). increasing(f;k) (x,y:k. x < y f(x) < f(y))
[-3]