A Proof of the Elementary Property of Connected Spaces

coq_topology.v

(******************************************************)
(** //// Topology Spaces  ////                        *)
(******************************************************)

Section Topology.


(*////////////////////////////////////////////////////*)
(** Axioms                                            *)
(*////////////////////////////////////////////////////*)

(* Definition : Subset (as a charectristic function) *)
Definition Subset (X : Set) : Type := X -> Prop.

(* Definition : Whole set *)
Definition whole (X : Set) : Subset X := fun (x : X) => x = x.

(* Definition : Empty set *)
Definition empty (X : Set) : Subset X := fun (x : X) => x <> x.

(* Predicate : incl S1 S2 <=> S1 is included in S2. *)
Inductive incl {X : Set} : Subset X -> Subset X -> Prop :=
    | Incl_intro : forall S1 S2 : Subset X,
                   (forall x : X, S1 x -> S2 x) ->
                   incl S1 S2.

(* Definition : Intersection (for families of subsets) *)
Definition bigcap {X : Set}
                  (I : Set) (index : I -> Subset X) : Subset X :=
    fun (x : X) => forall i : I, (index i) x.

(* Definition : Intersection (for pairs of two subsets) *)
Definition intsec {X : Set} (S1 S2 : Subset X) : Subset X :=
    let index (b : bool) := match b with
                            | true  => S1
                            | false => S2
                            end in
    bigcap bool index.

(* Definition : Union (for families of subsets) *)
Definition bigcup {X : Set}
                  (I : Set) (index : I -> Subset X) : Subset X :=
    fun (x : X) => exists i : I, (index i) x.

(* Definition : Union ()for pairs of two subsets *)
Definition union {X : Set} (S1 S2 : Subset X) : Subset X :=
    let index (b : bool) := match b with
                            | true  => S1
                            | false => S2
                            end in
    bigcup bool index.

(* Axiom : Topology space *)
Class TopSpace (X : Set) (Open : Subset X -> Prop) := {
    TS_whole :
        Open (whole X);
    TS_empty :
        Open (empty X);
    TS_intsec :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 ->
        Open (intsec U1 U2);
    TS_union :
        forall (I : Set) (index : I -> Subset X),
        (forall i : I, Open (index i)) ->
        Open (bigcup I index)
}.

(* Definition : Composition of functions *)
Definition composite {X Y Z : Set}
                     (g : Y -> Z) (f : X -> Y) : X -> Z :=
    fun (x : X) => g (f x).

(* Definition : Image *)
Definition image {X Y : Set}
                 (f : X -> Y) (U : Subset X) : Subset Y :=
    fun (y : Y) => exists x : X, U x /\ f x = y.

(* Definition : Preimage *)
Definition preimage {X Y : Set}
                    (f : X -> Y) (V : Subset Y) : Subset X :=
    fun (x : X) => V (f x).

(* Axiom : Continuous function *)
Class Continuous (X : Set) (XOpen : Subset X -> Prop)
                 (Y : Set) (YOpen : Subset Y -> Prop)
                 (f : X -> Y) := {
    Conti_TopSpace_l :>
        TopSpace X XOpen;
    Conti_TopSpace_r :>
        TopSpace Y YOpen;
    Conti_preim :
        forall V : Subset Y,
        YOpen V -> XOpen (preimage f V)
}.

(* Axiom : Connected Subset *)
Class Connected (X : Set) (Open : Subset X -> Prop)
                (S : Subset X) := {
    Conn_TopSpace :>
        TopSpace X Open;
    Conn_insep :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 -> incl S (union U1 U2) ->
        (exists x1 : X, (intsec S U1) x1) ->
        (exists x2 : X, (intsec S U2) x2) ->
        exists x : X, intsec S (intsec U1 U2) x
}.


(*////////////////////////////////////////////////////*)
(** Preliminaries                                     *)
(*////////////////////////////////////////////////////*)

(* Compatibility of intsec and /\ *)
Lemma intsec_and : forall {X : Set} (S1 S2 : Subset X) (x : X),
                   (intsec S1 S2) x <-> S1 x /\ S2 x.
Proof.
    intros X S1 S2 x.
    split.
    
        (* Direction -> *)
        intro H.
        unfold intsec in H.
        unfold bigcap in H.
        split.
        
            (* Proof : x is in S1. *)
            specialize H with true.
            simpl in H.
            apply H.
        
            (* Proof : x is in S2. *)
            specialize H with false.
            simpl in H.
            apply H.
    
        (* Direction <- *)
        intro H.
        unfold intsec.
        unfold bigcap.
        induction i as [ | ].
        
            (* Proof : x is in S1. *)
            apply H.
        
            (* Proof : x is in S2. *)
            apply H.
Qed.

(* Compatibility of union and \/ *)
Lemma union_or : forall {X : Set} (S1 S2 : Subset X) (x : X),
                 (union S1 S2) x <-> S1 x \/ S2 x.
Proof.
    intros X S1 S2 x.
    split.
    
        (* Derection -> *)
        intro H.
        unfold union in H.
        unfold bigcup in H.
        destruct H as [i H_i].
        induction i.
        
            (* Case : x is in S1. *)
            left.
            apply H_i.
        
            (* Case : x is in S2. *)
            right.
            apply H_i.
    
        (* Direction <- *)
        intro H.
        unfold union.
        unfold bigcup.
        destruct H as [H | H].
        
            (* Case : x is in S1. *)
            exists true.
            apply H.
        
            (* Case : x is in S2. *)
            exists false.
            apply H.
Qed.

(* If x belongs to S, then (f x) belongs to (image f S). *)
Lemma image_push : forall {X Y : Set} (S : Subset X)
                          (f : X -> Y) (x : X),
                   S x -> (image f S) (f x).
Proof.
    intros X Y S f x H.
    unfold image.
    exists x.
    split.
    
        (* Proof : x is in S. *)
        apply H.
    
        (* Proof : f x = f x *)
        reflexivity.
Qed.

(* If (f x) belongs to S, then x belongs to (preimage f S). *)
Lemma preimage_pull : forall {X Y : Set} (S : Subset Y)
                             (f : X -> Y) (x : X),
                      S (f x)-> preimage f S x.
Proof.
    intros X Y S f x H.
    unfold preimage.
    apply H.
Qed.


(*////////////////////////////////////////////////////*)
(** Proof : Connectedness                             *)
(*////////////////////////////////////////////////////*)

Section Connectedness.

(* Assumption : f : X -> Y is continuous, U is open in X. *)
Variables X Y : Set.
Variable XOpen : Subset X -> Prop.
Variable YOpen : Subset Y -> Prop.
Hypothesis X_TopSpace : TopSpace X XOpen.
Hypothesis Y_TopSpace : TopSpace Y YOpen.
Variable f : X -> Y.
Hypothesis f_Continuous : Continuous X XOpen Y YOpen f.
Variable U : Subset X.
Hypothesis U_Connected : Connected X XOpen U.

Instance image_Connected : Connected Y YOpen (image f U).
Proof.
    apply Build_Connected.
    
        (* Proof : (Y, YOpen) is a topology space. *)
        apply Y_TopSpace.
    
        (* Proof : Continuous images preserve connectedness. *)
        intros V1 V2 H_V1 H_V2 H_incl H_ne1 H_ne2.
        destruct H_ne1 as [y1 H_ne1].
        destruct H_ne2 as [y2 H_ne2].
        assert (exists x : X, (intsec U (intsec (preimage f V1)
                                                (preimage f V2)) x))
               as H_x.
        
            (* Proof of the assertion *)
            apply Conn_insep.
            
                (* Proof : (preimage f V1) is open. *)
                apply f_Continuous.
                apply H_V1.
            
                (* Proof : (preimage f V2) is open. *)
                apply f_Continuous.
                apply H_V2.
            
                (* Proof : U is included in the union of
                           (preimage f V1) and (preimage f V2)) *)
                apply Incl_intro.
                intros x H_x.
                apply union_or.
                inversion H_incl as [a b H_incl' d e].
                apply (image_push U f) in H_x.
                apply H_incl' in H_x.
                apply union_or in H_x.
                destruct H_x as [H_x | H_x].
                
                    (* Case : (f x) is in V1. *)
                    left.
                    apply H_x.
                
                    (* Case : (f x) is in V2. *)
                    right.
                    apply H_x.
            
                (* Proof : intersection of U and preimage f V1)
                           is nonempty *)
                apply intsec_and in H_ne1.
                destruct H_ne1 as [H_U H_y1].
                destruct H_U as [x1 H_x1].
                exists x1.
                apply intsec_and.
                split.
                
                    (* Proof : x1 is in U. *)
                    apply H_x1.
                
                    (* Proof : x1 is in (preimage f V1). *)
                    apply preimage_pull.
                    destruct H_x1 as [_ H_x1].
                    rewrite H_x1.
                    apply H_y1.
            
                (* Proof : intersection of U and preimage f V2)
                           is nonempty *)
                apply intsec_and in H_ne2.
                destruct H_ne2 as [H_U H_y2].
                destruct H_U as [x2 H_x2].
                exists x2.
                apply intsec_and.
                split.
                
                    (* Proof : x2 is in U. *)
                    apply H_x2.
                
                    (* Proof : x2 is in (preimage f V2). *)
                    apply preimage_pull.
                    destruct H_x2 as [_ H_x2].
                    rewrite H_x2.
                    apply H_y2.
        
        destruct H_x as [x H_x].
        exists (f x).
        apply intsec_and.
        apply intsec_and in H_x.
        destruct H_x as [H_x H_pre].
        apply intsec_and in H_pre.
        destruct H_pre as [H_pre1 H_pre2].
        split.
        
            (* Proof : (f x) is in (image f U) *)
            apply image_push.
            apply H_x.
        
        apply intsec_and.
        split.
        
            (* Proof : (f x) is in V1. *)
            apply H_pre1.
        
            (* Proof : (f x) is in V2. *)
            apply H_pre2.
Defined.

End Connectedness.

End Topology.