Library Stdlib.Reals.Rtopology

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import RList.
From Stdlib Require Import List.
From Stdlib Require Import Classical_Prop.
From Stdlib Require Import Classical_Pred_Type.
Local Open Scope R_scope.

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 : 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.

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.

Proof of Heine's theorem

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.