Library Coq.Reals.Rseries
Definition of sequence and properties
Section sequence.
Variable Un :
nat ->
R.
Boxed Fixpoint Rmax_N (
N:
nat) :
R :=
match N with
|
O =>
Un 0
|
S n =>
Rmax (
Un (
S n)) (
Rmax_N n)
end.
Definition EUn r :
Prop :=
exists i : nat, r = Un i.
Definition Un_cv (
l:
R) :
Prop :=
forall eps:
R,
eps > 0 ->
exists N : nat, (forall n:
nat, (
n >= N)%
nat ->
R_dist (
Un n)
l < eps).
Definition Cauchy_crit :
Prop :=
forall eps:
R,
eps > 0 ->
exists N : nat,
(forall n m:
nat,
(
n >= N)%
nat -> (
m >= N)%
nat ->
R_dist (
Un n) (
Un m)
< eps).
Definition Un_growing :
Prop :=
forall n:
nat,
Un n <= Un (
S n).
Lemma EUn_noempty :
exists r : R, EUn r.
Lemma Un_in_EUn :
forall n:
nat,
EUn (
Un n).
Lemma Un_bound_imp :
forall x:
R, (
forall n:
nat,
Un n <= x) ->
is_upper_bound EUn x.
Lemma growing_prop :
forall n m:
nat,
Un_growing -> (
n >= m)%
nat ->
Un n >= Un m.
classical is needed: not_all_not_ex
Definition of Power Series and properties