-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOrderTopology.v
166 lines (152 loc) · 3.57 KB
/
OrderTopology.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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
Require Export Subbases.
Require Export Relation_Definitions_Implicit.
Require Export SeparatednessAxioms.
Section OrderTopology.
Variable X:Type.
Variable R:relation X.
Hypothesis R_ord: order R.
Inductive order_topology_subbasis : Family X :=
| intro_lower_interval: forall x:X,
In order_topology_subbasis [ y:X | R y x /\ y <> x ]
| intro_upper_interval: forall x:X,
In order_topology_subbasis [ y:X | R x y /\ y <> x].
Definition OrderTopology : TopologicalSpace :=
Build_TopologicalSpace_from_subbasis X order_topology_subbasis.
Section if_total_order.
Hypothesis R_total: forall x y:X, R x y \/ R y x.
Lemma lower_closed_interval_closed: forall x:X,
closed [ y:X | R y x ] (X:=OrderTopology).
Proof.
intro.
red.
match goal with |- open ?U => cut (U = interior U) end.
intro.
rewrite H; apply interior_open.
apply Extensionality_Ensembles; split.
2:apply interior_deflationary.
intros y ?.
red in H.
red in H.
assert (R x y).
destruct (R_total x y); trivial.
contradiction H.
constructor; trivial.
exists ([z:X | R x z /\ z <> x]).
constructor; split.
apply (Build_TopologicalSpace_from_subbasis_subbasis
_ order_topology_subbasis).
constructor.
red; intros z ?.
destruct H1.
destruct H1.
intro.
destruct H3.
contradiction H2.
apply (ord_antisym R_ord); trivial.
constructor.
split; trivial.
intro.
contradiction H.
constructor.
destruct H1; apply (ord_refl R_ord).
Qed.
Lemma upper_closed_interval_closed: forall x:X,
closed [y:X | R x y] (X:=OrderTopology).
Proof.
intro.
red.
match goal with |- open ?U => cut (U = interior U) end.
intro.
rewrite H; apply interior_open.
apply Extensionality_Ensembles; split.
2:apply interior_deflationary.
intros y ?.
red in H.
red in H.
assert (R y x).
destruct (R_total x y); trivial.
contradiction H.
constructor; trivial.
exists ([z:X | R z x /\ z <> x]).
constructor; split.
apply (Build_TopologicalSpace_from_subbasis_subbasis
_ order_topology_subbasis).
constructor.
red; intros z ?.
destruct H1.
destruct H1.
intro.
destruct H3.
contradiction H2.
apply (ord_antisym R_ord); trivial.
constructor.
split; trivial.
intro.
contradiction H.
constructor.
destruct H1; apply (ord_refl R_ord).
Qed.
Lemma order_topology_Hausdorff: Hausdorff OrderTopology.
Proof.
red.
match goal with |- forall x y:point_set OrderTopology, ?P =>
cut (forall x y:point_set OrderTopology, R x y -> P)
end.
intros.
destruct (R_total x y).
exact (H x y H1 H0).
assert (y <> x).
auto.
destruct (H y x H1 H2) as [V [U [? [? [? []]]]]].
exists U; exists V; repeat split; trivial.
transitivity (Intersection V U); trivial.
apply Extensionality_Ensembles; split; red; intros.
destruct H8; constructor; trivial.
destruct H8; constructor; trivial.
intros.
pose proof (Build_TopologicalSpace_from_subbasis_subbasis
_ order_topology_subbasis).
destruct (classic (exists z:X, R x z /\ R z y /\ z <> x /\ z <> y)).
destruct H2 as [z [? [? []]]].
exists ([w:X | R w z /\ w <> z]);
exists ([w:X | R z w /\ w <> z]).
repeat split; trivial.
apply H1.
constructor.
apply H1.
constructor.
auto.
auto.
apply Extensionality_Ensembles; split; red; intros.
destruct H6.
destruct H6.
destruct H7.
destruct H6.
destruct H7.
contradiction H8.
apply (ord_antisym R_ord); trivial.
destruct H6.
exists ([w:X | R w y /\ w <> y]);
exists ([w:X | R x w /\ w <> x]).
repeat split.
apply H1.
constructor.
apply H1.
constructor.
trivial.
trivial.
trivial.
auto.
apply Extensionality_Ensembles; split; red; intros.
destruct H3.
destruct H3.
destruct H4.
destruct H3.
destruct H4.
contradiction H2.
exists x0; repeat split; trivial.
destruct H3.
Qed.
End if_total_order.
End OrderTopology.
Implicit Arguments OrderTopology [[X]].