Thm* P,Q:(T![](FONT/dash.png) Prop), R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop).
Thm* R preserves P ![](FONT/eq.png) R preserves Q ![](FONT/eq.png) R preserves P Q | [and_preserved_by] |
Thm* k: , P:( k![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* (( i: k. P(i)) ![](FONT/if_big.png) 0<search(k;P))
Thm* & (0<search(k;P) ![](FONT/eq.png) P(search(k;P)-1) & ( j: k. j<search(k;P)-1 ![](FONT/eq.png) P(j))) | [search_property] |
Thm* k: , x,y,i: k. (y, x)((y, x)(i)) = i | [flip_twice] |
Thm* k: , x,y: k. (y, x) o (y, x) = ( x.x) | [flip_inverse] |
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![](FONT/dash.png) ![](FONT/then_med.png) ), i: (n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n) | [sum_switch] |
Thm* f:(T![](FONT/dash.png) T), m:(T![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* ( x:T. m(f(x)) m(x) & (m(f(x)) = m(x) ![](FONT/eq.png) f(x) = x))
Thm* ![](FONT/eq.png)
Thm* ( x:T. n: . f(f^n(x)) = f^n(x)) | [iteration_terminates] |
Thm* f:(T![](FONT/dash.png) T), n:![](FONT/nat.png) , x:T. f(f^n-1(x)) = f^n(x) | [fun_exp_add1_sub] |
Thm* f:(T![](FONT/dash.png) T), n: , x:T. f(f^n(x)) = f^n+1(x) | [fun_exp_add1] |
Thm* n,m: , f:(T![](FONT/dash.png) T). f^n+m = f^n o f^m | [fun_exp_add] |
Thm* n: , h,f:(T![](FONT/dash.png) T). f^n o h = primrec(n;h; i,g. f o g) | [fun_exp_compose] |
Thm* P:(T![](FONT/dash.png) Prop), R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop).
Thm* R1 preserves P ![](FONT/eq.png) R2 preserves P ![](FONT/eq.png) R1 R2 preserves P | [preserved_by_or] |
Thm* R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop).
Thm* (Sym x,y:T. x R1 y) ![](FONT/eq.png) (Sym x,y:T. x R2 y) ![](FONT/eq.png) (Sym x,y:T. x (R1 R2) y) | [symmetric_rel_or] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). (Sym x,y:T. x R y) ![](FONT/eq.png) (Sym x,y:T. x (R^*) y) | [rel_star_symmetric] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y:T. (x R^*^-1 y) ![](FONT/if_big.png) (x (R^-1^*) y) | [rel_inverse_star] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), n: , x,y:T. (x R^n^-1 y) ![](FONT/if_big.png) (x R^-1^n y) | [rel_inverse_exp] |
Thm* x,y:T, R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). x = y ![](FONT/eq.png) (x (R^*) y) | [rel_star_weakening] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y,z:T. (x R y) ![](FONT/eq.png) (y (R^*) z) ![](FONT/eq.png) (x (R^*) z) | [rel_star_trans] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y:T. (x R y) ![](FONT/eq.png) (x (R^*) y) | [rel_rel_star] |
Thm* E:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y:T. EquivRel(T)(_1 E _2) ![](FONT/eq.png) (x (E^*) y) ![](FONT/eq.png) (x E y) | [rel_star_of_equiv] |
Thm* R,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop).
Thm* Trans(T)(R2(_1,_2))
Thm* ![](FONT/eq.png)
Thm* ( x,y:T. (x R y) ![](FONT/eq.png) (x R2 y)) ![](FONT/eq.png) ( x,y:T. (x (R^*) y) ![](FONT/eq.png) (x R2 y) x = y) | [rel_star_closure] |
Thm* P:(T![](FONT/dash.png) Prop), R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). R preserves P ![](FONT/eq.png) R^* preserves P | [preserved_by_star] |
Thm* R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y:T. R1 => R2 ![](FONT/eq.png) (x (R1^*) y) ![](FONT/eq.png) (x (R2^*) y) | [rel_star_monotonic] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y,z:T. (x (R^*) y) ![](FONT/eq.png) (y (R^*) z) ![](FONT/eq.png) (x (R^*) z) | [rel_star_transitivity] |
Thm* R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). R1 => R2 ![](FONT/eq.png) R1^* => R2^* | [rel_star_monotone] |
Thm* P:(T![](FONT/dash.png) Prop), R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop).
Thm* ( x,y:T. (x R1 y) ![](FONT/eq.png) (x R2 y)) ![](FONT/eq.png) R2 preserves P ![](FONT/eq.png) R1 preserves P | [preserved_by_monotone] |
Thm* n: , T:Type, R1,R2:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). R1 => R2 ![](FONT/eq.png) R1^n => R2^n | [rel_exp_monotone] |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), m,n: , x,y,z:T. (x R^m y) ![](FONT/eq.png) (y R^n z) ![](FONT/eq.png) (x R^m+n z) | [rel_exp_add] |
Thm* k,n: , R:( n![](FONT/dash.png) ![](FONT/then_med.png) n![](FONT/dash.png) Prop). ( i,j: n. Dec(i R j)) ![](FONT/eq.png) ( i,j: n. Dec(i R^k j)) | [decidable__rel_exp] |
Thm* n: , T:Type, R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). R^n T![](FONT/dash.png) T![](FONT/dash.png) Prop | [rel_exp_wf] |
Thm* n,m: , f,g:( n![](FONT/dash.png) ![](FONT/then_med.png) m![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* ( x: n, y: m. f(x,y) = g(x,y))
Thm* ![](FONT/eq.png)
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![](FONT/dash.png) ![](FONT/then_med.png) m![](FONT/dash.png) ![](FONT/then_med.png) ), d: .
Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d
Thm* ![](FONT/eq.png)
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![](FONT/dash.png) ![](FONT/then_med.png) m![](FONT/dash.png) ![](FONT/then_med.png) ), x1,x2: n, y1,y2: m.
Thm* x1 = x2 y1 = y2
Thm* ![](FONT/eq.png)
Thm* ( x: n, y: m. (x = x1 & y = y1) ![](FONT/eq.png) (x = x2 & y = y2) ![](FONT/eq.png) f(x,y) = 0)
Thm* ![](FONT/eq.png)
Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2) | [pair_support_double_sum] |
Thm* n: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) ), 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![](FONT/dash.png) ![](FONT/then_med.png) ), m,k: n.
Thm* m = k
Thm* ![](FONT/eq.png)
Thm* ( x: n. x = m ![](FONT/eq.png) x = k ![](FONT/eq.png) f(x) = 0) ![](FONT/eq.png) sum(f(x) | x < n) = f(m)+f(k) | [pair_support] |
Thm* n,m: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) m). Inj( n; m; f) ![](FONT/eq.png) n m | [pigeon-hole] |
Thm* n,k: , c:( n![](FONT/dash.png) ![](FONT/then_med.png) k).
Thm* p:( k![](FONT/dash.png) ( List)).
Thm* sum(||p(j)|| | j < k) = n
Thm* & ( j: k, x,y: ||p(j)||. x<y ![](FONT/eq.png) (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![](FONT/dash.png) ![](FONT/then_med.png) ), m: n.
Thm* ( x: n. x = m ![](FONT/eq.png) f(x) = 0) ![](FONT/eq.png) sum(f(x) | x < n) = f(m) | [singleton_support_sum] |
Thm* n: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) ). ( x: n. f(x) = 0) ![](FONT/eq.png) sum(f(x) | x < n) = 0 | [empty_support] |
Thm* n: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) ), 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![](FONT/dash.png) ![](FONT/then_med.png) ), p:( k![](FONT/dash.png) ![](FONT/then_med.png) ).
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![](FONT/dash.png) ![](FONT/then_med.png) ). ( x: k. b f(x)) ![](FONT/eq.png) b k sum(f(x) | x < k) | [sum_lower_bound] |
Thm* k,b: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) ). ( x: k. f(x) b) ![](FONT/eq.png) sum(f(x) | x < k) b k | [sum_bound] |
Thm* k: , f,g:( k![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* ( x: k. f(x) g(x)) ![](FONT/eq.png) sum(f(x) | x < k) sum(g(x) | x < k) | [sum_le] |
Thm* n: , f,g:( n![](FONT/dash.png) ![](FONT/then_med.png) ), d: .
Thm* sum(f(x)-g(x) | x < n) = d ![](FONT/eq.png) sum(f(x) | x < n) = sum(g(x) | x < n)+d | [sum_difference] |
Thm* n: , f,g:( n![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* ( i: n. f(i) = g(i)) ![](FONT/eq.png) 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![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* sum(f(x) | x < n)+sum(g(x) | x < n) = sum(f(x)+g(x) | x < n) | [sum_linear] |
Thm* n: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) ). ( x: n. 0 f(x)) ![](FONT/eq.png) 0 sum(f(x) | x < n) | [non_neg_sum] |
Thm* m: , P:( m![](FONT/dash.png) Prop).
Thm* ( i: m. Dec(P(i)))
Thm* ![](FONT/eq.png)
Thm* ( n,k: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) m), g:( k![](FONT/dash.png) ![](FONT/then_med.png) 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![](FONT/dash.png) ![](FONT/then_med.png) m), x: m. f[n:=x] (n+1)![](FONT/dash.png) ![](FONT/then_med.png) m | [fappend_wf] |
Thm* n: , f,g:( n![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* increasing(f;n) ![](FONT/eq.png) nondecreasing(g;n) ![](FONT/eq.png) increasing(fadd(f;g);n) | [fadd_increasing] |
Thm* k: , x: . nondecreasing( i.x;k) | [const_nondecreasing] |
Thm* n,m: , b:T, c:( (n+m)![](FONT/dash.png) T![](FONT/dash.png) 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![](FONT/dash.png) T![](FONT/dash.png) T). primrec(n;b;c) T | [primrec_wf] |
Thm* k: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) k).
Thm* 0<k
Thm* ![](FONT/eq.png)
Thm* Bij( k; k; f)
Thm* ![](FONT/eq.png)
Thm* f(k-1) = k-1 ![](FONT/eq.png) f (k-1)![](FONT/dash.png) ![](FONT/then_med.png) (k-1) & Bij( (k-1); (k-1); f) | [bijection_restriction] |
Thm* m,n,k: , f:( n![](FONT/dash.png) ![](FONT/then_med.png) m), g:( k![](FONT/dash.png) ![](FONT/then_med.png) m).
Thm* increasing(f;n)
Thm* ![](FONT/eq.png)
Thm* increasing(g;k)
Thm* ![](FONT/eq.png)
Thm* ( i: m. ( j: n. i = f(j)) ( j: k. i = g(j)))
Thm* ![](FONT/eq.png)
Thm* ( j1: n, j2: k. f(j1) = g(j2)) ![](FONT/eq.png) m = n+k ![](FONT/nat.png) | [disjoint_increasing_onto] |
Thm* k,m: . ( f:( k![](FONT/dash.png) ![](FONT/then_med.png) m). Inj( k; m; f)) ![](FONT/eq.png) k m | [injection_le] |
Thm* k: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) ), x: k. increasing(f;k) ![](FONT/eq.png) f(0)+x f(x) | [increasing_lower_bound] |
Thm* k: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) k). increasing(f;k) ![](FONT/eq.png) ( i: k. f(i) = i) | [increasing_is_id] |
Thm* k,m: . ( f:( k![](FONT/dash.png) ![](FONT/then_med.png) m). increasing(f;k)) ![](FONT/eq.png) k m | [increasing_le] |
Thm* k,m: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) m). increasing(f;k) ![](FONT/eq.png) Inj( k; m; f) | [increasing_inj] |
Thm* k,m: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) m), g:( m![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* increasing(f;k) ![](FONT/eq.png) increasing(g;m) ![](FONT/eq.png) increasing(g o f;k) | [compose_increasing] |
Thm* k: , f:( k![](FONT/dash.png) ![](FONT/then_med.png) ). increasing(f;k) ![](FONT/eq.png) ( x,y: k. x<y ![](FONT/eq.png) f(x)<f(y)) | [increasing_implies] |
Thm* k: . increasing( i.i;k) | [id_increasing] |
Def (ternary) R preserves P == x,y,z:T. P(x) ![](FONT/eq.png) P(y) ![](FONT/eq.png) R(x,y,z) ![](FONT/eq.png) P(z) | [preserved_by2] |
Def R preserves P == x,y:T. P(x) ![](FONT/eq.png) (x R y) ![](FONT/eq.png) P(y) | [preserved_by] |
Def R1 => R2 == x,y:T. (x R1 y) ![](FONT/eq.png) (x R2 y) | [rel_implies] |
Def nondecreasing(f;k) == i: (k-1). f(i) f(i+1) | [nondecreasing] |