Library Coq.Reals.Rtopology
General definitions and propositions
Definition included (
D1 D2:R ->
Prop) :
Prop :=
forall x:R,
D1 x ->
D2 x.
Definition disc (
x:R) (
delta:posreal) (
y:R) :
Prop :=
Rabs (
y -
x) <
delta.
Definition neighbourhood (
V:R ->
Prop) (
x:R) :
Prop :=
exists delta :
posreal,
included (
disc x delta)
V.
Definition open_set (
D:R ->
Prop) :
Prop :=
forall x:R,
D x ->
neighbourhood D x.
Definition complementary (
D:R ->
Prop) (
c:R) :
Prop := ~
D c.
Definition closed_set (
D:R ->
Prop) :
Prop :=
open_set (
complementary D).
Definition intersection_domain (
D1 D2:R ->
Prop) (
c:R) :
Prop :=
D1 c /\
D2 c.
Definition union_domain (
D1 D2:R ->
Prop) (
c:R) :
Prop :=
D1 c \/
D2 c.
Definition interior (
D:R ->
Prop) (
x:R) :
Prop :=
neighbourhood D x.
Lemma interior_P1 :
forall D:R ->
Prop,
included (
interior D)
D.
Lemma interior_P2 :
forall D:R ->
Prop,
open_set D ->
included D (
interior D).
Definition point_adherent (
D:R ->
Prop) (
x:R) :
Prop :=
forall V:R ->
Prop,
neighbourhood V x ->
exists y :
R,
intersection_domain V D y.
Definition adherence (
D:R ->
Prop) (
x:R) :
Prop :=
point_adherent D x.
Lemma adherence_P1 :
forall D:R ->
Prop,
included D (
adherence D).
Lemma included_trans :
forall D1 D2 D3:R ->
Prop,
included D1 D2 ->
included D2 D3 ->
included D1 D3.
Lemma interior_P3 :
forall D:R ->
Prop,
open_set (
interior D).
Lemma complementary_P1 :
forall D:R ->
Prop,
~ (
exists y :
R,
intersection_domain D (
complementary D)
y).
Lemma adherence_P2 :
forall D:R ->
Prop,
closed_set D ->
included (
adherence D)
D.
Lemma adherence_P3 :
forall D:R ->
Prop,
closed_set (
adherence D).
Definition eq_Dom (
D1 D2:R ->
Prop) :
Prop :=
included D1 D2 /\
included D2 D1.
Infix "=_D" :=
eq_Dom (
at level 70,
no associativity).
Lemma open_set_P1 :
forall D:R ->
Prop,
open_set D <->
D =_D
interior D.
Lemma closed_set_P1 :
forall D:R ->
Prop,
closed_set D <->
D =_D
adherence D.
Lemma neighbourhood_P1 :
forall (
D1 D2:R ->
Prop) (
x:R),
included D1 D2 ->
neighbourhood D1 x ->
neighbourhood D2 x.
Lemma open_set_P2 :
forall D1 D2:R ->
Prop,
open_set D1 ->
open_set D2 ->
open_set (
union_domain D1 D2).
Lemma open_set_P3 :
forall D1 D2:R ->
Prop,
open_set D1 ->
open_set D2 ->
open_set (
intersection_domain D1 D2).
Lemma open_set_P4 :
open_set (
fun x:R =>
False).
Lemma open_set_P5 :
open_set (
fun x:R =>
True).
Lemma disc_P1 :
forall (
x:R) (
del:posreal),
open_set (
disc x del).
Lemma continuity_P1 :
forall (
f:R ->
R) (
x:R),
continuity_pt f x <->
(
forall W:R ->
Prop,
neighbourhood W (
f x) ->
exists V :
R ->
Prop,
neighbourhood V x /\ (
forall y:R,
V y ->
W (
f y))).
Definition image_rec (
f:R ->
R) (
D:R ->
Prop) (
x:R) :
Prop :=
D (
f x).
Lemma continuity_P2 :
forall (
f:R ->
R) (
D:R ->
Prop),
continuity f ->
open_set D ->
open_set (
image_rec f D).
Lemma continuity_P3 :
forall f:R ->
R,
continuity f <->
(
forall D:R ->
Prop,
open_set D ->
open_set (
image_rec f D)).
Theorem Rsepare :
forall x y:R,
x <>
y ->
exists V :
R ->
Prop,
(
exists W :
R ->
Prop,
neighbourhood V x /\
neighbourhood W y /\ ~ (
exists y :
R,
intersection_domain V W y)).
Record family :
Type :=
mkfamily
{
ind :
R ->
Prop;
f :>
R ->
R ->
Prop;
cond_fam :
forall x:R, (
exists y :
R,
f x y) ->
ind x}.
Definition family_open_set (
f:family) :
Prop :=
forall x:R,
open_set (
f x).
Definition domain_finite (
D:R ->
Prop) :
Prop :=
exists l :
Rlist, (
forall x:R,
D x <->
In x l).
Definition family_finite (
f:family) :
Prop :=
domain_finite (
ind f).
Definition covering (
D:R ->
Prop) (
f:family) :
Prop :=
forall x:R,
D x ->
exists y :
R,
f y x.
Definition covering_open_set (
D:R ->
Prop) (
f:family) :
Prop :=
covering D f /\
family_open_set f.
Definition covering_finite (
D:R ->
Prop) (
f:family) :
Prop :=
covering D f /\
family_finite f.
Lemma restriction_family :
forall (
f:family) (
D:R ->
Prop) (
x:R),
(
exists y :
R, (
fun z1 z2:R =>
f z1 z2 /\
D z1)
x y) ->
intersection_domain (
ind f)
D x.
Definition subfamily (
f:family) (
D:R ->
Prop) :
family :=
mkfamily (
intersection_domain (
ind f)
D) (
fun x y:R =>
f x y /\
D x)
(
restriction_family f D).
Definition compact (
X:R ->
Prop) :
Prop :=
forall f:family,
covering_open_set X f ->
exists D :
R ->
Prop,
covering_finite X (
subfamily f D).
Lemma family_P1 :
forall (
f:family) (
D:R ->
Prop),
family_open_set f ->
family_open_set (
subfamily f D).
Definition bounded (
D:R ->
Prop) :
Prop :=
exists m :
R, (
exists M :
R, (
forall x:R,
D x ->
m <=
x <=
M)).
Lemma open_set_P6 :
forall D1 D2:R ->
Prop,
open_set D1 ->
D1 =_D
D2 ->
open_set D2.
Lemma compact_P1 :
forall X:R ->
Prop,
compact X ->
bounded X.
Lemma compact_P2 :
forall X:R ->
Prop,
compact X ->
closed_set X.
Lemma compact_EMP :
compact (
fun _:R =>
False).
Lemma compact_eqDom :
forall X1 X2:R ->
Prop,
compact X1 ->
X1 =_D
X2 ->
compact X2.
Borel-Lebesgue's lemma
Lemma compact_P3 :
forall a b:R,
compact (
fun c:R =>
a <=
c <=
b).
Lemma compact_P4 :
forall X F:R ->
Prop,
compact X ->
closed_set F ->
included F X ->
compact F.
Lemma compact_P5 :
forall X:R ->
Prop,
closed_set X ->
bounded X ->
compact X.
Lemma compact_carac :
forall X:R ->
Prop,
compact X <->
closed_set X /\
bounded X.
Definition image_dir (
f:R ->
R) (
D:R ->
Prop) (
x:R) :
Prop :=
exists y :
R,
x =
f y /\
D y.
Lemma continuity_compact :
forall (
f:R ->
R) (
X:R ->
Prop),
(
forall x:R,
continuity_pt f x) ->
compact X ->
compact (
image_dir f X).
Lemma Rlt_Rminus :
forall a b:R,
a <
b -> 0 <
b -
a.
Lemma prolongement_C0 :
forall (
f:R ->
R) (
a b:R),
a <=
b ->
(
forall c:R,
a <=
c <=
b ->
continuity_pt f c) ->
exists g :
R ->
R,
continuity g /\ (
forall c:R,
a <=
c <=
b ->
g c =
f c).
Lemma continuity_ab_maj :
forall (
f:R ->
R) (
a b:R),
a <=
b ->
(
forall c:R,
a <=
c <=
b ->
continuity_pt f c) ->
exists Mx :
R, (
forall c:R,
a <=
c <=
b ->
f c <=
f Mx) /\
a <=
Mx <=
b.
Lemma continuity_ab_min :
forall (
f:R ->
R) (
a b:R),
a <=
b ->
(
forall c:R,
a <=
c <=
b ->
continuity_pt f c) ->
exists mx :
R, (
forall c:R,
a <=
c <=
b ->
f mx <=
f c) /\
a <=
mx <=
b.
Proof of Bolzano-Weierstrass theorem
Definition ValAdh (
un:nat ->
R) (
x:R) :
Prop :=
forall (
V:R ->
Prop) (
N:nat),
neighbourhood V x ->
exists p :
nat, (
N <=
p)%nat /\
V (
un p).
Definition intersection_family (
f:family) (
x:R) :
Prop :=
forall y:R,
ind f y ->
f y x.
Lemma ValAdh_un_exists :
forall (
un:nat ->
R) (
D:=fun
x:R =>
exists n :
nat,
x =
INR n)
(
f:=
fun x:R =>
adherence
(
fun y:R => (
exists p :
nat,
y =
un p /\
x <=
INR p) /\
D x))
(
x:R), (
exists y :
R,
f x y) ->
D x.
Definition ValAdh_un (
un:nat ->
R) :
R ->
Prop :=
let D :=
fun x:R =>
exists n :
nat,
x =
INR n in
let f :=
fun x:R =>
adherence
(
fun y:R => (
exists p :
nat,
y =
un p /\
x <=
INR p) /\
D x)
in
intersection_family (
mkfamily D f (
ValAdh_un_exists un)).
Lemma ValAdh_un_prop :
forall (
un:nat ->
R) (
x:R),
ValAdh un x <->
ValAdh_un un x.
Lemma adherence_P4 :
forall F G:R ->
Prop,
included F G ->
included (
adherence F) (
adherence G).
Definition family_closed_set (
f:family) :
Prop :=
forall x:R,
closed_set (
f x).
Definition intersection_vide_in (
D:R ->
Prop) (
f:family) :
Prop :=
forall x:R,
(
ind f x ->
included (
f x)
D) /\
~ (
exists y :
R,
intersection_family f y).
Definition intersection_vide_finite_in (
D:R ->
Prop)
(
f:family) :
Prop :=
intersection_vide_in D f /\
family_finite f.
Lemma compact_P6 :
forall X:R ->
Prop,
compact X ->
(
exists z :
R,
X z) ->
forall g:family,
family_closed_set g ->
intersection_vide_in X g ->
exists D :
R ->
Prop,
intersection_vide_finite_in X (
subfamily g D).
Theorem Bolzano_Weierstrass :
forall (
un:nat ->
R) (
X:R ->
Prop),
compact X -> (
forall n:nat,
X (
un n)) ->
exists l :
R,
ValAdh un l.
Definition uniform_continuity (
f:R ->
R) (
X:R ->
Prop) :
Prop :=
forall eps:posreal,
exists delta :
posreal,
(
forall x y:R,
X x ->
X y ->
Rabs (
x -
y) <
delta ->
Rabs (
f x -
f y) <
eps).
Lemma is_lub_u :
forall (
E:R ->
Prop) (
x y:R),
is_lub E x ->
is_lub E y ->
x =
y.
Lemma domain_P1 :
forall X:R ->
Prop,
~ (
exists y :
R,
X y) \/
(
exists y :
R,
X y /\ (
forall x:R,
X x ->
x =
y)) \/
(
exists x :
R, (
exists y :
R,
X x /\
X y /\
x <>
y)).
Theorem Heine :
forall (
f:R ->
R) (
X:R ->
Prop),
compact X ->
(
forall x:R,
X x ->
continuity_pt f x) ->
uniform_continuity f X.