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 limit_in (
X X':Metric_Space) (
f:Base
X ->
Base X')
(
D:Base
X ->
Prop) (
x0:Base
X) (
l:Base
X') :=
forall eps:R,
eps > 0 ->
exists alp :
R,
alp > 0 /\
(
forall x:Base
X,
D x /\
dist X x x0 <
alp ->
dist X' (
f x)
l <
eps).
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.