-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathConnectedness.v
122 lines (112 loc) · 2.58 KB
/
Connectedness.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
Require Export TopologicalSpaces.
Definition clopen {X:TopologicalSpace} (S:Ensemble (point_set X))
: Prop :=
open S /\ closed S.
Definition connected (X:TopologicalSpace) : Prop :=
forall S:Ensemble (point_set X), clopen S ->
S = Empty_set \/ S = Full_set.
Require Export Continuity.
Lemma connected_img: forall {X Y:TopologicalSpace}
(f:point_set X -> point_set Y),
connected X -> continuous f -> surjective f -> connected Y.
Proof.
intros.
red; intros.
destruct (H (inverse_image f S)).
split.
apply H0.
apply H2.
red.
rewrite <- inverse_image_complement.
apply H0.
apply H2.
left.
apply Extensionality_Ensembles; split; red; intros.
destruct (H1 x).
assert (In Empty_set x0).
rewrite <- H3.
constructor.
rewrite H5.
trivial.
destruct H6.
destruct H4.
right.
apply Extensionality_Ensembles; split; red; intros.
constructor.
destruct (H1 x).
rewrite <- H5.
assert (In (inverse_image f S) x0).
rewrite H3; constructor.
destruct H6; trivial.
Qed.
Require Export SubspaceTopology.
Lemma connected_union: forall {X:TopologicalSpace}
{A:Type} (S:IndexedFamily A (point_set X)),
(forall a:A, connected (SubspaceTopology (S a))) ->
Inhabited (IndexedIntersection S) ->
IndexedUnion S = Full_set -> connected X.
Proof.
intros.
pose (inc := fun (a:A) => subspace_inc (S a)).
destruct H0.
destruct H0.
red; intros.
assert (forall a:A, clopen (inverse_image (inc a) S0)).
intro.
split.
apply subspace_inc_continuous.
apply H2.
red.
rewrite <- inverse_image_complement.
apply subspace_inc_continuous.
apply H2.
destruct (classic (In S0 x)).
right.
assert (forall a:A, inverse_image (inc a) S0 = Full_set).
intro.
destruct (H a _ (H3 a)).
assert (In (@Empty_set (point_set (SubspaceTopology (S a))))
(exist _ x (H0 a))).
rewrite <- H5.
constructor.
simpl.
trivial.
destruct H6.
trivial.
apply Extensionality_Ensembles; split; red; intros.
constructor.
assert (In (IndexedUnion S) x0).
rewrite H1; constructor.
destruct H7.
assert (In (@Full_set (point_set (SubspaceTopology (S a))))
(exist _ x0 H7)).
constructor.
rewrite <- H5 in H8.
destruct H8.
simpl in H8.
trivial.
left.
assert (forall a:A, inverse_image (inc a) S0 = Empty_set).
intros.
destruct (H a _ (H3 a)).
trivial.
assert (In (@Full_set (point_set (SubspaceTopology (S a))))
(exist _ x (H0 a))).
constructor.
rewrite <- H5 in H6.
destruct H6.
simpl in H6.
contradiction H4.
apply Extensionality_Ensembles; split; red; intros.
assert (In (IndexedUnion S) x0).
rewrite H1; constructor.
destruct H7.
assert (In (@Empty_set (point_set (SubspaceTopology (S a))))
(exist _ x0 H7)).
rewrite <- H5.
constructor.
simpl.
trivial.
destruct H8.
destruct H6.
Qed.