Thm* k: , P:( k  ).
Thm* (( i: k. P(i))  0<search(k;P))
Thm* & (0<search(k;P)  P(search(k;P)-1) & ( j: k. j<search(k;P)-1  P(j))) | [search_property] |
Thm* k: , i,j: k. Bij( k; k; (i, j)) | [flip_bijection] |
Thm* k: , i,j: k. (i, j) = (j, i) | [flip_symmetry] |
Thm* n: , f:( n  ), i: (n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n) | [sum_switch] |
Thm* f:(T T), m:(T  ).
Thm* ( x:T. m(f(x)) m(x) & (m(f(x)) = m(x)  f(x) = x))
Thm* 
Thm* ( x:T. n: . f(f^n(x)) = f^n(x)) | [iteration_terminates] |
Thm* f:(T T), n: , x:T. f(f^n(x)) = f^n+1(x) | [fun_exp_add1] |
Thm* n,m: , f:(T T). f^n+m = f^n o f^m | [fun_exp_add] |
Thm* n: , h,f:(T T). f^n o h = primrec(n;h; i,g. f o g) | [fun_exp_compose] |
Thm* R:(T T Prop), n: , x,y:T. (x R^n^-1 y)  (x R^-1^n y) | [rel_inverse_exp] |
Thm* n: , T:Type, R1,R2:(T T Prop). R1 => R2  R1^n => R2^n | [rel_exp_monotone] |
Thm* R:(T T Prop), m,n: , x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z) | [rel_exp_add] |
Thm* k,n: , R:( n  n Prop). ( i,j: n. Dec(i R j))  ( i,j: n. Dec(i R^k j)) | [decidable__rel_exp] |
Thm* n: , T:Type, R:(T T Prop). R^n T T Prop | [rel_exp_wf] |
Thm* n,m: , f,g:( n  m  ).
Thm* ( x: n, y: m. f(x,y) = g(x,y))
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m) | [double_sum_functionality] |
Thm* n,m: , f,g:( n  m  ), d: .
Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d | [double_sum_difference] |
Thm* n,m: , f:( n  m  ), x1,x2: n, y1,y2: m.
Thm* x1 = x2 y1 = y2
Thm* 
Thm* ( x: n, y: m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0)
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2) | [pair_support_double_sum] |
Thm* n: , f:( n  ), m: (n+1).
Thm* sum(f(x) | x < n) = sum(f(x) | x < m)+sum(f(x+m) | x < n-m) | [sum_split] |
Thm* n: , f:( n  ), m,k: n.
Thm* m = k
Thm* 
Thm* ( x: n. x = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k) | [pair_support] |
Thm* n,m: , f:( n  m). Inj( n; m; f)  n m | [pigeon-hole] |
Thm* n,k: , c:( n  k).
Thm* p:( k ( List)).
Thm* sum(||p(j)|| | j < k) = n
Thm* & ( j: k, x,y: ||p(j)||. x<y  (p(j))[x]>(p(j))[y])
Thm* & ( j: k, x: ||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j) | [finite-partition] |
Thm* n: , f:( n  ), m: n.
Thm* ( x: n. x = m  f(x) = 0)  sum(f(x) | x < n) = f(m) | [singleton_support_sum] |
Thm* n: , f:( n  ). ( x: n. f(x) = 0)  sum(f(x) | x < n) = 0 | [empty_support] |
Thm* n: , f:( n  ), m: n.
Thm* sum(f(x) | x < n) = f(m)+sum(if x= m 0 else f(x) fi | x < n) | [isolate_summand] |
Thm* k: , f,g:( k  ), p:( k  ).
Thm* sum(if p(i) f(i)+g(i) else f(i) fi | i < k)
Thm* =
Thm* sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) | [sum-ite] |
Thm* k,b: , f:( k  ). ( x: k. b f(x))  b k sum(f(x) | x < k) | [sum_lower_bound] |
Thm* k,b: , f:( k  ). ( x: k. f(x) b)  sum(f(x) | x < k) b k | [sum_bound] |
Thm* k: , f,g:( k  ).
Thm* ( x: k. f(x) g(x))  sum(f(x) | x < k) sum(g(x) | x < k) | [sum_le] |
Thm* n: , f,g:( n  ), d: .
Thm* sum(f(x)-g(x) | x < n) = d  sum(f(x) | x < n) = sum(g(x) | x < n)+d | [sum_difference] |
Thm* n: , f,g:( n  ).
Thm* ( i: n. f(i) = g(i))  sum(f(x) | x < n) = sum(g(x) | x < n) | [sum_functionality] |
Thm* n: , a: . sum(a | x < n) = a n | [sum_constant] |
Thm* n: , f,g:( n  ).
Thm* sum(f(x) | x < n)+sum(g(x) | x < n) = sum(f(x)+g(x) | x < n) | [sum_linear] |
Thm* n: , f:( n  ). ( x: n. 0 f(x))  0 sum(f(x) | x < n) | [non_neg_sum] |
Thm* m: , P:( m Prop).
Thm* ( i: m. Dec(P(i)))
Thm* 
Thm* ( n,k: , f:( n  m), g:( k  m).
Thm* (increasing(f;n)
Thm* (& increasing(g;k)
Thm* (& ( i: n. P(f(i)))
Thm* (& ( j: k. P(g(j)))
Thm* (& ( i: m. ( j: n. i = f(j)) ( j: k. i = g(j)))) | [increasing_split] |
Thm* n,m: , f:( n  m), x: m. f[n:=x] (n+1)  m | [fappend_wf] |
Thm* n: , f,g:( n  ).
Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n) | [fadd_increasing] |
Thm* k: , x: . nondecreasing( i.x;k) | [const_nondecreasing] |
Thm* n,m: , b:T, c:( (n+m) T T).
Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c); i,t. c(i+m,t)) | [primrec_add] |
Thm* T:Type, n: , b:T, c:( n T T). primrec(n;b;c) T | [primrec_wf] |
Thm* k: , f:( k  k).
Thm* 0<k
Thm* 
Thm* Bij( k; k; f)
Thm* 
Thm* f(k-1) = k-1  f (k-1)  (k-1) & Bij( (k-1); (k-1); f) | [bijection_restriction] |
Thm* m,n,k: , f:( n  m), g:( k  m).
Thm* increasing(f;n)
Thm* 
Thm* increasing(g;k)
Thm* 
Thm* ( i: m. ( j: n. i = f(j)) ( j: k. i = g(j)))
Thm* 
Thm* ( j1: n, j2: k. f(j1) = g(j2))  m = n+k  | [disjoint_increasing_onto] |
Thm* k,m: . ( f:( k  m). Inj( k; m; f))  k m | [injection_le] |
Thm* k: , f:( k  ), x: k. increasing(f;k)  f(0)+x f(x) | [increasing_lower_bound] |
Thm* k: , f:( k  k). increasing(f;k)  ( i: k. f(i) = i) | [increasing_is_id] |
Thm* k,m: . ( f:( k  m). increasing(f;k))  k m | [increasing_le] |
Thm* k,m: , f:( k  m). increasing(f;k)  Inj( k; m; f) | [increasing_inj] |
Thm* k,m: , f:( k  m), g:( m  ).
Thm* increasing(f;k)  increasing(g;m)  increasing(g o f;k) | [compose_increasing] |
Thm* k: , f:( k  ). increasing(f;k)  ( x,y: k. x<y  f(x)<f(y)) | [increasing_implies] |
Thm* k: . increasing( i.i;k) | [id_increasing] |
Def (R^*)(x,y) == n: . x R^n y | [rel_star] |