Selected Objects
Introduction | Introductory Remarks |
def | is_ident
|
(u is an identity element for operation f on A)
is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x |
THM | binary_ident_unique
|
A binary operation has at most one identity value.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u,v:A. is_ident(A; f; u) ![](FONT/eq.png) is_ident(A; f; v) ![](FONT/eq.png) u = v |
THM | intmul_ident_one
|
is_ident( ; ( x,y. x y); 1) |
THM | natmul_ident_one
|
is_ident( ; ( x,y. x y); 1) |
THM | intadd_ident_zero
|
is_ident( ; ( x,y. x+y); 0) |
THM | natadd_ident_zero
|
is_ident( ; ( x,y. x+y); 0) |
def | is_assoc
|
Associativity of a function
is_assoc(A; x,z.f(x;z)) == x,y,z:A. f(x;f(y;z)) = f(f(x;y);z) A |
def | is_assoc_sep
|
Associativity of a function
is_assoc_sep(A; f) == is_assoc(A; x,y.(f(x,y))) |
THM | is_assoc_intmul
|
is_assoc_sep( ; ( x,y. x y)) |
THM | is_assoc_intadd
|
is_assoc_sep( ; ( x,y. x+y)) |
def | is_commutative
|
Commutativity of a function
is_commutative(A; x,z.f(x;z)) == x,z:A. f(x;z) = f(z;x) A |
def | is_commutative_sep
|
Commutativity of a function
is_commutative_sep(A; f) == is_commutative(A; x,z.(f(x,z))) |
THM | is_commutative_sep_intmul
|
is_commutative_sep( ; ( x,y. x y)) |
THM | is_commutative_sep_intadd
|
is_commutative_sep( ; ( x,y. x+y)) |
THM | split_int_domain
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
( b:{...a}. P(a,b))
![](FONT/eq.png)
(( b:{...a}. P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b))) ![](FONT/eq.png) ( b: . P(a,b)) |
THM | all_int_pairs_via_all_splits
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop).
( a: , b:{...a}. P(a,b))
![](FONT/eq.png)
( a: . ( b:{...a}. P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b))) ![](FONT/eq.png) ( a,b: . P(a,b)) |
THM | int_seg_upper_ind
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
( b:{a...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b)) |
THM | split_int_domain_by_norm_lower
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
( b:{...a}. P(a,a) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b)) ![](FONT/eq.png) ( b: . P(a,b)) |
THM | int_segs_from_base_by_upper_ind
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
( b:{...a}. P(a,b))
![](FONT/eq.png)
( b:{a+1...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b: . P(a,b)) |
THM | all_int_segs_by_upper_ind
|
P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop).
( a: , b:{...a}. P(a,b))
![](FONT/eq.png)
( a: , b:{a+1...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( a,b: . P(a,b)) |
def | iter_via_intseg
|
Iteration of a binary operator over a finite sequence of values. Some special cases of this iteration operator include sum, product and exponentiation:
i:{a..b }. e(i)
|
|
Iter( x,y. x+y;0) i:{a..b }. e(i)
|
i: b. e(i)
|
|
Iter( x,y. x+y;0) i:{0..b }. e(i)
|
i:{a..b }. e(i)
|
|
Iter( x,y. x y;1) i:{a..b }. e(i)
|
i: b. e(i)
|
|
Iter( x,y. x y;1) i:{0..b }. e(i)
|
e b
|
|
Iter( x,y. x y;1) :{0..b }. e
|
Or i:{a..b }. e(i)
|
|
Iter( x,y. x y;False) i:{a..b }. e(i)
|
Or i: b. e(i)
|
|
Iter( x,y. x y;False) i:{0..b }. e(i)
|
And i:{a..b }. e(i)
|
|
Iter( x,y. x & y;True) i:{a..b }. e(i)
|
And i: b. e(i)
|
|
Iter( x,y. x & y;True) i:{0..b }. e(i)
|
Iter(f;u) i:{a..b }. e(i)
== if a< b f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) else u fi
(recursive) |
THM | exponent_zero
|
x: . x 0 = 1 |
THM | exponent_one
|
x: . x 1 = x |
THM | iter_via_intseg_null
|
Iteration over a null sequence is the identity element.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A). b a ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = u |
THM | iter_via_intseg_nullnorm
|
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
b a ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{a..a }. e(i)) |
THM | iter_via_intseg_singleton
|
Iteration over a singleton is just the value for the one index.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_ident(A; f; u)
![](FONT/eq.png)
( a,b: , e:({a..b }![](FONT/dash.png) A). a+1 = b ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = e(a)) |
THM | sum_via_intseg_singleton
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). a+1 = b ![](FONT/eq.png) ( i:{a..b }. e(i)) = e(a) |
THM | mul_via_intseg_singleton
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). a+1 = b ![](FONT/eq.png) ( i:{a..b }. e(i)) = e(a) |
THM | iter_via_intseg_notnull
|
Splitting the last element from the range of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
a<b
![](FONT/eq.png)
( c: .
(b = c+1 ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..c }. e(i)),e(c))) |
THM | mul_via_intseg_notnull
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c)) |
THM | sum_via_intseg_notnull
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)) |
THM | iter_via_intseg_split_last
|
Splitting the last element from the domain of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
a<b ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) |
THM | iter_via_intseg_all_units
|
Iterating over only identity values gives the identity value itself.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_ident(A; f; u)
![](FONT/eq.png)
( a,b: , e:({a..b }![](FONT/dash.png) A).
(( i:{a..b }. e(i) = u) ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = u) |
THM | mul_via_intseg_one
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). ( i:{a..b }. e(i) = 1) ![](FONT/eq.png) ( i:{a..b }. e(i)) = 1 |
THM | one_exponentiation
|
x: . 1 x = 1 |
THM | iter_via_intseg_shift_rw
|
Shifting the range of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A), k: .
(Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{a+k..b+k }. e(j-k)) |
THM | iter_via_intseg_shift
|
Shifting the range of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b,c,d: .
b-a = d-c
![](FONT/eq.png)
( e:({a..b }![](FONT/dash.png) A), g:({c..d }![](FONT/dash.png) A).
(( i:{a..b }, j:{c..d }. j-i = c-a ![](FONT/eq.png) e(i) = g(j) A)
(![](FONT/eq.png)
((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{c..d }. g(j))) |
THM | iter_via_intseg_comp_binop
|
Joining two iterations pairwise.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_commutative_sep(A; f)
![](FONT/eq.png)
is_ident(A; f; u)
![](FONT/eq.png)
is_assoc_sep(A; f)
![](FONT/eq.png)
( a,b: , e,g:({a..b }![](FONT/dash.png) A).
(f((Iter(f;u) i:{a..b }. e(i)),Iter(f;u) i:{a..b }. g(i))
(=
((Iter(f;u) i:{a..b }. f(e(i),g(i)))
( A) |
THM | add_via_intseg_addends
|
Adding two summations pairwise.
a,b: , f,g:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
( i:{a..b }. f(i))+( i:{a..b }. g(i)) = ( i:{a..b }. f(i)+g(i)) |
THM | iter_via_intseg_split_mid
|
Splitting the range of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_ident(A; f; u)
![](FONT/eq.png)
is_assoc_sep(A; f)
![](FONT/eq.png)
( a,c,b: , e:({a..b }![](FONT/dash.png) A).
(a c
(![](FONT/eq.png)
(c b
(![](FONT/eq.png)
((Iter(f;u) i:{a..b }. e(i))
(=
(f((Iter(f;u) i:{a..c }. e(i)),Iter(f;u) i:{c..b }. e(i))) |
THM | iter_via_intseg_amputate_units
|
Removing units from the ends of the range of iteration preserves the result.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_ident(A; f; u)
![](FONT/eq.png)
is_assoc_sep(A; f)
![](FONT/eq.png)
( a,b: , c:{a...b}, d:{c..b }, e:({a..b }![](FONT/dash.png) A).
(( i:{a..b }. i<c d i ![](FONT/eq.png) e(i) = u)
(![](FONT/eq.png)
((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{c..d }. e(i))) |
THM | iter_via_intseg_split_pluck
|
Splitting the range of iteration.
f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
is_ident(A; f; u)
![](FONT/eq.png)
is_assoc_sep(A; f)
![](FONT/eq.png)
( a,c,b: , e:({a..b }![](FONT/dash.png) A).
(a c
(![](FONT/eq.png)
(c<b
(![](FONT/eq.png)
((Iter(f;u) i:{a..b }. e(i))
(=
(f((Iter(f;u) i:{a..c }. e(i)),f(e(c),Iter(f;u) i:{c+1..b }. e(i)))) |
THM | sum_via_intseg_split_pluck
|
Splitting the range of iteration.
a,c,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a c
![](FONT/eq.png)
c<b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)+( i:{c+1..b }. e(i)) |
THM | mul_via_intseg_split_pluck
|
Splitting the range of iteration.
a,c,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a c
![](FONT/eq.png)
c<b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c) ( i:{c+1..b }. e(i)) |
THM | components_divide_iter_mul
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ), i:{a..b }. e(i) | ( i:{a..b }. e(i)) |
THM | sum_via_intseg_split_mid
|
Splitting the range of iteration.
a,c,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a c ![](FONT/eq.png) c b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+( i:{c..b }. e(i)) |
THM | mul_via_intseg_split_mid
|
Splitting the range of iteration.
a,c,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a c ![](FONT/eq.png) c b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) ( i:{c..b }. e(i)) |
THM | sum_exponent
|
i: , x,y: . i x i y = i (x+y) |
THM | mul_via_intseg_split_last
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a<b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i)) e(b-1) |
THM | mul_via_intseg_factors
|
a,b: , f,g:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
( i:{a..b }. f(i)) ( i:{a..b }. g(i)) = ( i:{a..b }. f(i) g(i)) |
THM | exp_reduce1
|
Corollary to mul via intseg factors
a,b,c: . (a b) c = a c b c |
THM | sum_via_intseg_split_last
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
a<b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i))+e(b-1) |
THM | and_via_all_intseg_notnull
|
a,b: , P:({a..b }![](FONT/dash.png) Prop).
a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..c }. P(i)) & P(c))) |
THM | and_via_all_intseg_split_last
|
a,b: , P:({a..b }![](FONT/dash.png) Prop).
a<b ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..(b-1) }. P(i)) & P(b-1)) |
THM | all_intseg_vs_iter_and
|
Universal quantification over a finite range is iterated conjunction.
a,b: , P:({a..b }![](FONT/dash.png) Prop). ( i:{a..b }. P(i)) ![](FONT/if_big.png) (And i:{a..b }. P(i)) |
THM | or_via_exist_intseg_notnull
|
a,b: , P:({a..b }![](FONT/dash.png) Prop).
a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..c }. P(i)) P(c))) |
THM | or_via_exist_intseg_split_last
|
a,b: , P:({a..b }![](FONT/dash.png) Prop).
a<b ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..(b-1) }. P(i)) P(b-1)) |
THM | exist_intseg_null
|
a,b: , P:({a..b }![](FONT/dash.png) Prop). b a ![](FONT/eq.png) ( i:{a..b }. P(i)) |
THM | exist_intseg_vs_iter_or
|
Existential quantification over a finite range is iterated disjunction.
a,b: , P:({a..b }![](FONT/dash.png) Prop). ( i:{a..b }. P(i)) ![](FONT/if_big.png) (Or i:{a..b }. P(i)) |
THM | iter_nat_prod_one_iff_factors_one
|
An iterated product is one iff each value is one.
e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). ( i:{a..b }. e(i)) = 1 ![](FONT/if_big.png) ( i:{a..b }. e(i) = 1) |
THM | iter_prod_zero_iff_factor_zero
|
( i:{a..b }. e(i)) = 0 ![](FONT/if_big.png) ( i:{a..b }. e(i) = 0) |
THM | zero_ann_iter_via_intseg
|
( i:{a..b }. e(i) = 0) ![](FONT/eq.png) ( i:{a..b }. e(i)) = 0 |
def | factorial_tail_via_iter
|
k!m == i:{k-m..k }. i+1 |
THM | factorial_tail_split_mid
|
n,m,k: . n k-m ![](FONT/eq.png) m k ![](FONT/eq.png) k!(n+m) = (k-m)!n k!m |
THM | factorial_tail_via_iter_null
|
m,k: . m = 0 ![](FONT/eq.png) k!m = 1 ![](FONT/nat.png) |
THM | factorial_tail_via_iter_zero
|
m,k: . k<m ![](FONT/eq.png) k!m = 0 ![](FONT/nat.png) |
THM | factorial_tail_via_iter_step
|
m,k: . 1 m k ![](FONT/eq.png) ( k',m': . k' = k-1 ![](FONT/eq.png) m' = m-1 ![](FONT/eq.png) k!m = k k'!m' ) |
THM | factorial_tail_via_iter_step_rw
|
m,k: . 1 m k ![](FONT/eq.png) k!m = k (k-1)!(m-1) ![](FONT/nat.png) |
def | factorial_via_iter
|
k! == k!k |
THM | factorial_ratio
|
m,k: . m k ![](FONT/eq.png) k! = (k-m)! k!m |
THM | factorial_ratio2
|
Definition of a commonly used ratio of factorials.
m,k: . m k ![](FONT/eq.png) k!m = ((k!) ((k-m)!)) |
THM | mul_via_intseg_null
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). b a ![](FONT/eq.png) ( i:{a..b }. e(i)) = 1 |
THM | sum_via_intseg_null
|
a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). b a ![](FONT/eq.png) ( i:{a..b }. e(i)) = 0 |