Skip to content

Instantly share code, notes, and snippets.

@y-taka-23
Created January 6, 2013 12:24
Show Gist options
  • Save y-taka-23/4466805 to your computer and use it in GitHub Desktop.
Save y-taka-23/4466805 to your computer and use it in GitHub Desktop.
A Proof of the Elementary Property of Connected Spaces
(******************************************************)
(** //// 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment