n,m:
, f:((n-1)
(m-1)). Inj((n-1); (m-1); f) 
Inj(n; m; f[n-1:=m-1])n,m:, f:((n-1)(m-1)). increasing(f;n-1) increasing(f[n-1:=m-1];n)
n
x else f(i) fi
is mentioned by
| Thm* n,m:, f:((n-1)(m-1)). Inj((n-1); (m-1); f) Inj(n; m; f[n-1:=m-1]) | [fappend-inject] |
| Thm* n,m:, f:((n-1)(m-1)). increasing(f;n-1) increasing(f[n-1:=m-1];n) | [fappend-increasing] |
Try larger context:
Graphs