Library Coq.Reals.Rtopology
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import RList.
Require Import List.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Local Open Scope R_scope.
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 : list R, (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 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.
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 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.
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.