Library Coq.Reals.Rlimit
Definition of the limit
Lemma eps2_Rgt_R0 :
forall eps:
R,
eps > 0 ->
eps * / 2
> 0.
Lemma eps2 :
forall eps:
R,
eps * / 2
+ eps * / 2
= eps.
Lemma eps4 :
forall eps:
R,
eps * / (2
+ 2
) + eps * / (2
+ 2
) = eps * / 2.
Lemma Rlt_eps2_eps :
forall eps:
R,
eps > 0 ->
eps * / 2
< eps.
Lemma Rlt_eps4_eps :
forall eps:
R,
eps > 0 ->
eps * / (2
+ 2
) < eps.
Lemma prop_eps :
forall r:
R, (
forall eps:
R,
eps > 0 ->
r < eps) ->
r <= 0.
Definition mul_factor (
l l´:
R) :=
/ (1
+ (Rabs l + Rabs l´)).
Lemma mul_factor_wd :
forall l l´:
R, 1
+ (Rabs l + Rabs l´) <> 0.
Lemma mul_factor_gt :
forall eps l l´:
R,
eps > 0 ->
eps * mul_factor l l´ > 0.
Lemma mul_factor_gt_f :
forall eps l l´:
R,
eps > 0 ->
Rmin 1 (
eps * mul_factor l l´)
> 0.
Definition Dgf (
Df Dg:
R ->
Prop) (
f:
R ->
R) (
x:
R) :=
Df x /\ Dg (
f x).
Definition limit1_in (
f:
R ->
R) (
D:
R ->
Prop) (
l x0:
R) :
Prop :=
limit_in R_met R_met f D x0 l.
Lemma tech_limit :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
l x0:
R),
D x0 ->
limit1_in f D l x0 ->
l = f x0.
Lemma tech_limit_contr :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
l x0:
R),
D x0 ->
l <> f x0 ->
~ limit1_in f D l x0.
Lemma lim_x :
forall (
D:
R ->
Prop) (
x0:
R),
limit1_in (
fun x:
R =>
x)
D x0 x0.
Lemma limit_plus :
forall (
f g:
R ->
R) (
D:
R ->
Prop) (
l l´ x0:
R),
limit1_in f D l x0 ->
limit1_in g D l´ x0 ->
limit1_in (
fun x:
R =>
f x + g x)
D (
l + l´)
x0.
Lemma limit_Ropp :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
l x0:
R),
limit1_in f D l x0 ->
limit1_in (
fun x:
R =>
- f x)
D (
- l)
x0.
Lemma limit_minus :
forall (
f g:
R ->
R) (
D:
R ->
Prop) (
l l´ x0:
R),
limit1_in f D l x0 ->
limit1_in g D l´ x0 ->
limit1_in (
fun x:
R =>
f x - g x)
D (
l - l´)
x0.
Lemma limit_free :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
x x0:
R),
limit1_in (
fun h:
R =>
f x)
D (
f x)
x0.
Lemma limit_mul :
forall (
f g:
R ->
R) (
D:
R ->
Prop) (
l l´ x0:
R),
limit1_in f D l x0 ->
limit1_in g D l´ x0 ->
limit1_in (
fun x:
R =>
f x * g x)
D (
l * l´)
x0.
Definition adhDa (
D:
R ->
Prop) (
a:
R) :
Prop :=
forall alp:
R,
alp > 0 ->
exists x :
R, D x /\ R_dist x a < alp.
Lemma single_limit :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
l l´ x0:
R),
adhDa D x0 ->
limit1_in f D l x0 ->
limit1_in f D l´ x0 ->
l = l´.
Lemma limit_comp :
forall (
f g:
R ->
R) (
Df Dg:
R ->
Prop) (
l l´ x0:
R),
limit1_in f Df l x0 ->
limit1_in g Dg l´ l ->
limit1_in (
fun x:
R =>
g (
f x)) (
Dgf Df Dg f)
l´ x0.
Lemma limit_inv :
forall (
f:
R ->
R) (
D:
R ->
Prop) (
l x0:
R),
limit1_in f D l x0 ->
l <> 0 ->
limit1_in (
fun x:
R =>
/ f x)
D (
/ l)
x0.