Thm* P,Q:(T Prop), R:(T T Prop).
Thm* R preserves P  R preserves Q  R preserves P Q | [and_preserved_by] |
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* 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* P:(T Prop), R1,R2:(T T Prop).
Thm* R1 preserves P  R2 preserves P  R1 R2 preserves P | [preserved_by_or] |
Thm* R1,R2:(T T Prop).
Thm* (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1 R2) y) | [symmetric_rel_or] |
Thm* R:(T T Prop). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y) | [rel_star_symmetric] |
Thm* x,y:T, R:(T T Prop). x = y  (x (R^*) y) | [rel_star_weakening] |
Thm* R:(T T Prop), x,y,z:T. (x R y)  (y (R^*) z)  (x (R^*) z) | [rel_star_trans] |
Thm* R:(T T Prop), x,y:T. (x R y)  (x (R^*) y) | [rel_rel_star] |
Thm* E:(T T Prop), x,y:T. EquivRel(T)(_1 E _2)  (x (E^*) y)  (x E y) | [rel_star_of_equiv] |
Thm* R,R2:(T T Prop).
Thm* Trans(T)(R2(_1,_2))
Thm* 
Thm* ( x,y:T. (x R y)  (x R2 y))  ( x,y:T. (x (R^*) y)  (x R2 y) x = y) | [rel_star_closure] |
Thm* P:(T Prop), R:(T T Prop). R preserves P  R^* preserves P | [preserved_by_star] |
Thm* R1,R2:(T T Prop), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y) | [rel_star_monotonic] |
Thm* R:(T T Prop), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z) | [rel_star_transitivity] |
Thm* R1,R2:(T T Prop). R1 => R2  R1^* => R2^* | [rel_star_monotone] |
Thm* P:(T Prop), R1,R2:(T T Prop).
Thm* ( x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P | [preserved_by_monotone] |
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,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,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* 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: , 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: , f,g:( n  ).
Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n) | [fadd_increasing] |
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] |
Def (ternary) R preserves P == x,y,z:T. P(x)  P(y)  R(x,y,z)  P(z) | [preserved_by2] |
Def R preserves P == x,y:T. P(x)  (x R y)  P(y) | [preserved_by] |
Def R1 => R2 == x,y:T. (x R1 y)  (x R2 y) | [rel_implies] |