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* 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* 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* 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,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,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* 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: , 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: , 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: , 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] |
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] |