author | wenzelm |
Fri, 12 Apr 2019 22:09:25 +0200 | |
changeset 70136 | f03a01a18c6e |
parent 69939 | 812ce526da33 |
child 70178 | 4900351361b0 |
permissions | -rw-r--r-- |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
1 |
(* Author: L C Paulson, University of Cambridge |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
2 |
Author: Amine Chaieb, University of Cambridge |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
3 |
Author: Robert Himmelmann, TU Muenchen |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
4 |
Author: Brian Huffman, Portland State University |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
5 |
*) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
6 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
7 |
section \<open>Abstract Topology 2\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
8 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
9 |
theory Abstract_Topology_2 |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
10 |
imports |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
11 |
Elementary_Topology |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
12 |
Abstract_Topology |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
13 |
"HOL-Library.Indicator_Function" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
14 |
begin |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
15 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
16 |
text \<open>Combination of Elementary and Abstract Topology\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
17 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
18 |
(* FIXME: move elsewhere *) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
19 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
20 |
lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
21 |
apply auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
22 |
apply (rule_tac x="d/2" in exI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
23 |
apply auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
24 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
25 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
26 |
lemma approachable_lt_le2: \<comment> \<open>like the above, but pushes aside an extra formula\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
27 |
"(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
28 |
apply auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
29 |
apply (rule_tac x="d/2" in exI, auto) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
30 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
31 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
32 |
lemma triangle_lemma: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
33 |
fixes x y z :: real |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
34 |
assumes x: "0 \<le> x" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
35 |
and y: "0 \<le> y" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
36 |
and z: "0 \<le> z" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
37 |
and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
38 |
shows "x \<le> y + z" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
39 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
40 |
have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
41 |
using z y by simp |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
42 |
with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
43 |
by (simp add: power2_eq_square field_simps) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
44 |
from y z have yz: "y + z \<ge> 0" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
45 |
by arith |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
46 |
from power2_le_imp_le[OF th yz] show ?thesis . |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
47 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
48 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
49 |
lemma isCont_indicator: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
50 |
fixes x :: "'a::t2_space" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
51 |
shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
52 |
proof auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
53 |
fix x |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
54 |
assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
55 |
with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
56 |
(\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
57 |
show False |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
58 |
proof (cases "x \<in> A") |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
59 |
assume x: "x \<in> A" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
60 |
hence "indicator A x \<in> ({0<..<2} :: real set)" by simp |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
61 |
hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
62 |
using 1 open_greaterThanLessThan by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
63 |
then guess U .. note U = this |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
64 |
hence "\<forall>y\<in>U. indicator A y > (0::real)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
65 |
unfolding greaterThanLessThan_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
66 |
hence "U \<subseteq> A" using indicator_eq_0_iff by force |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
67 |
hence "x \<in> interior A" using U interiorI by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
68 |
thus ?thesis using fr unfolding frontier_def by simp |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
69 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
70 |
assume x: "x \<notin> A" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
71 |
hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
72 |
hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
73 |
using 1 open_greaterThanLessThan by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
74 |
then guess U .. note U = this |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
75 |
hence "\<forall>y\<in>U. indicator A y < (1::real)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
76 |
unfolding greaterThanLessThan_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
77 |
hence "U \<subseteq> -A" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
78 |
hence "x \<in> interior (-A)" using U interiorI by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
79 |
thus ?thesis using fr interior_complement unfolding frontier_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
80 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
81 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
82 |
assume nfr: "x \<notin> frontier A" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
83 |
hence "x \<in> interior A \<or> x \<in> interior (-A)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
84 |
by (auto simp: frontier_def closure_interior) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
85 |
thus "isCont ((indicator A)::'a \<Rightarrow> real) x" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
86 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
87 |
assume int: "x \<in> interior A" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
88 |
then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
89 |
hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
90 |
hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
91 |
thus ?thesis using U continuous_on_eq_continuous_at by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
92 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
93 |
assume ext: "x \<in> interior (-A)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
94 |
then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
95 |
then have "continuous_on U (indicator A)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
96 |
using continuous_on_topological by (auto simp: subset_iff) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
97 |
thus ?thesis using U continuous_on_eq_continuous_at by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
98 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
99 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
100 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
101 |
lemma closedin_limpt: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
102 |
"closedin (top_of_set T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
103 |
apply (simp add: closedin_closed, safe) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
104 |
apply (simp add: closed_limpt islimpt_subset) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
105 |
apply (rule_tac x="closure S" in exI, simp) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
106 |
apply (force simp: closure_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
107 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
108 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
109 |
lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (top_of_set S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
110 |
by (meson closedin_limpt closed_subset closedin_closed_trans) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
111 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
112 |
lemma connected_closed_set: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
113 |
"closed S |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
114 |
\<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
115 |
unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
116 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
117 |
text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
118 |
have to intersect.\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
119 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
120 |
lemma connected_as_closed_union: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
121 |
assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
122 |
shows "A \<inter> B \<noteq> {}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
123 |
by (metis assms closed_Un connected_closed_set) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
124 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
125 |
lemma closedin_subset_trans: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
126 |
"closedin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
127 |
closedin (top_of_set T) S" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
128 |
by (meson closedin_limpt subset_iff) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
129 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
130 |
lemma openin_subset_trans: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
131 |
"openin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
132 |
openin (top_of_set T) S" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
133 |
by (auto simp: openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
134 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
135 |
lemma closedin_compact: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
136 |
"\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
137 |
by (metis closedin_closed compact_Int_closed) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
138 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
139 |
lemma closedin_compact_eq: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
140 |
fixes S :: "'a::t2_space set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
141 |
shows |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
142 |
"compact S |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
143 |
\<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
144 |
compact T \<and> T \<subseteq> S)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
145 |
by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
146 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
147 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
148 |
subsection \<open>Closure\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
149 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
150 |
lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
151 |
by (auto simp: closure_of_def closure_def islimpt_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
152 |
|
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
153 |
lemma closure_openin_Int_closure: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
154 |
assumes ope: "openin (top_of_set U) S" and "T \<subseteq> U" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
155 |
shows "closure(S \<inter> closure T) = closure(S \<inter> T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
156 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
157 |
obtain V where "open V" and S: "S = U \<inter> V" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
158 |
using ope using openin_open by metis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
159 |
show "closure (S \<inter> closure T) \<subseteq> closure (S \<inter> T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
160 |
proof (clarsimp simp: S) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
161 |
fix x |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
162 |
assume "x \<in> closure (U \<inter> V \<inter> closure T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
163 |
then have "V \<inter> closure T \<subseteq> A \<Longrightarrow> x \<in> closure A" for A |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
164 |
by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
165 |
then have "x \<in> closure (T \<inter> V)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
166 |
by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
167 |
then show "x \<in> closure (U \<inter> V \<inter> T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
168 |
by (metis \<open>T \<subseteq> U\<close> inf.absorb_iff2 inf_assoc inf_commute) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
169 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
170 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
171 |
show "closure (S \<inter> T) \<subseteq> closure (S \<inter> closure T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
172 |
by (meson Int_mono closure_mono closure_subset order_refl) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
173 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
174 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
175 |
corollary infinite_openin: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
176 |
fixes S :: "'a :: t1_space set" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
177 |
shows "\<lbrakk>openin (top_of_set U) S; x \<in> S; x islimpt U\<rbrakk> \<Longrightarrow> infinite S" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
178 |
by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
179 |
|
69622 | 180 |
lemma closure_Int_ballI: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
181 |
assumes "\<And>U. \<lbrakk>openin (top_of_set S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}" |
69622 | 182 |
shows "S \<subseteq> closure T" |
183 |
proof (clarsimp simp: closure_iff_nhds_not_empty) |
|
184 |
fix x and A and V |
|
185 |
assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}" |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
186 |
then have "openin (top_of_set S) (A \<inter> V \<inter> S)" |
69622 | 187 |
by (auto simp: openin_open intro!: exI[where x="V"]) |
188 |
moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close> |
|
189 |
by auto |
|
190 |
ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}" |
|
191 |
by (rule assms) |
|
192 |
with \<open>T \<inter> A = {}\<close> show False by auto |
|
193 |
qed |
|
194 |
||
195 |
||
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
196 |
subsection \<open>Frontier\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
197 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
198 |
lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
199 |
by (auto simp: interior_of_def interior_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
200 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
201 |
lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
202 |
by (auto simp: frontier_of_def frontier_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
203 |
|
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
204 |
lemma connected_Int_frontier: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
205 |
"\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
206 |
apply (simp add: frontier_interiors connected_openin, safe) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
207 |
apply (drule_tac x="s \<inter> interior t" in spec, safe) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
208 |
apply (drule_tac [2] x="s \<inter> interior (-t)" in spec) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
209 |
apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
210 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
211 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
212 |
subsection \<open>Compactness\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
213 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
214 |
lemma openin_delete: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
215 |
fixes a :: "'a :: t1_space" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
216 |
shows "openin (top_of_set u) s |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
217 |
\<Longrightarrow> openin (top_of_set u) (s - {a})" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
218 |
by (metis Int_Diff open_delete openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
219 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
220 |
lemma compact_eq_openin_cover: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
221 |
"compact S \<longleftrightarrow> |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
222 |
(\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
223 |
(\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
224 |
proof safe |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
225 |
fix C |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
226 |
assume "compact S" and "\<forall>c\<in>C. openin (top_of_set S) c" and "S \<subseteq> \<Union>C" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
227 |
then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
228 |
unfolding openin_open by force+ |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
229 |
with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
230 |
by (meson compactE) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
231 |
then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
232 |
by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
233 |
then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
234 |
next |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
235 |
assume 1: "\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
236 |
(\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
237 |
show "compact S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
238 |
proof (rule compactI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
239 |
fix C |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
240 |
let ?C = "image (\<lambda>T. S \<inter> T) C" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
241 |
assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
242 |
then have "(\<forall>c\<in>?C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>?C" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
243 |
unfolding openin_open by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
244 |
with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
245 |
by metis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
246 |
let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
247 |
have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
248 |
proof (intro conjI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
249 |
from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
250 |
by (fast intro: inv_into_into) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
251 |
from \<open>finite D\<close> show "finite ?D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
252 |
by (rule finite_imageI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
253 |
from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
254 |
apply (rule subset_trans, clarsimp) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
255 |
apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
256 |
apply (erule rev_bexI, fast) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
257 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
258 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
259 |
then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
260 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
261 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
262 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
263 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
264 |
subsection \<open>Continuity\<close> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
265 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
266 |
lemma interior_image_subset: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
267 |
assumes "inj f" "\<And>x. continuous (at x) f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
268 |
shows "interior (f ` S) \<subseteq> f ` (interior S)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
269 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
270 |
fix x assume "x \<in> interior (f ` S)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
271 |
then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
272 |
then have "x \<in> f ` S" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
273 |
then obtain y where y: "y \<in> S" "x = f y" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
274 |
have "open (f -` T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
275 |
using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
276 |
moreover have "y \<in> vimage f T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
277 |
using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
278 |
moreover have "vimage f T \<subseteq> S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
279 |
using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
280 |
ultimately have "y \<in> interior S" .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
281 |
with \<open>x = f y\<close> show "x \<in> f ` interior S" .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
282 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
283 |
|
70136 | 284 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Equality of continuous functions on closure and related results\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
285 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
286 |
lemma continuous_closedin_preimage_constant: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
287 |
fixes f :: "_ \<Rightarrow> 'b::t1_space" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
288 |
shows "continuous_on S f \<Longrightarrow> closedin (top_of_set S) {x \<in> S. f x = a}" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
289 |
using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
290 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
291 |
lemma continuous_closed_preimage_constant: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
292 |
fixes f :: "_ \<Rightarrow> 'b::t1_space" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
293 |
shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
294 |
using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
295 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
296 |
lemma continuous_constant_on_closure: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
297 |
fixes f :: "_ \<Rightarrow> 'b::t1_space" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
298 |
assumes "continuous_on (closure S) f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
299 |
and "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
300 |
and "x \<in> closure S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
301 |
shows "f x = a" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
302 |
using continuous_closed_preimage_constant[of "closure S" f a] |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
303 |
assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
304 |
unfolding subset_eq |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
305 |
by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
306 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
307 |
lemma image_closure_subset: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
308 |
assumes contf: "continuous_on (closure S) f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
309 |
and "closed T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
310 |
and "(f ` S) \<subseteq> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
311 |
shows "f ` (closure S) \<subseteq> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
312 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
313 |
have "S \<subseteq> {x \<in> closure S. f x \<in> T}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
314 |
using assms(3) closure_subset by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
315 |
moreover have "closed (closure S \<inter> f -` T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
316 |
using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
317 |
ultimately have "closure S = (closure S \<inter> f -` T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
318 |
using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
319 |
then show ?thesis by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
320 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
321 |
|
70136 | 322 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
323 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
324 |
definition constant_on (infixl "(constant'_on)" 50) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
325 |
where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
326 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
327 |
lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
328 |
unfolding constant_on_def by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
329 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
330 |
lemma injective_not_constant: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
331 |
fixes S :: "'a::{perfect_space} set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
332 |
shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
333 |
unfolding constant_on_def |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
334 |
by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
335 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
336 |
lemma constant_on_closureI: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
337 |
fixes f :: "_ \<Rightarrow> 'b::t1_space" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
338 |
assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
339 |
shows "f constant_on (closure S)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
340 |
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
341 |
by metis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
342 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
343 |
|
70136 | 344 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
345 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
346 |
lemma continuous_on_Un_local: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
347 |
"\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t; |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
348 |
continuous_on s f; continuous_on t f\<rbrakk> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
349 |
\<Longrightarrow> continuous_on (s \<union> t) f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
350 |
unfolding continuous_on closedin_limpt |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
351 |
by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
352 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
353 |
lemma continuous_on_cases_local: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
354 |
"\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t; |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
355 |
continuous_on s f; continuous_on t g; |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
356 |
\<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk> |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
357 |
\<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
358 |
by (rule continuous_on_Un_local) (auto intro: continuous_on_eq) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
359 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
360 |
lemma continuous_on_cases_le: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
361 |
fixes h :: "'a :: topological_space \<Rightarrow> real" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
362 |
assumes "continuous_on {t \<in> s. h t \<le> a} f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
363 |
and "continuous_on {t \<in> s. a \<le> h t} g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
364 |
and h: "continuous_on s h" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
365 |
and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
366 |
shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
367 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
368 |
have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
369 |
by force |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
370 |
have 1: "closedin (top_of_set s) (s \<inter> h -` atMost a)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
371 |
by (rule continuous_closedin_preimage [OF h closed_atMost]) |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
372 |
have 2: "closedin (top_of_set s) (s \<inter> h -` atLeast a)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
373 |
by (rule continuous_closedin_preimage [OF h closed_atLeast]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
374 |
have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
375 |
by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
376 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
377 |
apply (rule continuous_on_subset [of s, OF _ order_refl]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
378 |
apply (subst s) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
379 |
apply (rule continuous_on_cases_local) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
380 |
using 1 2 s assms apply (auto simp: eq) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
381 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
382 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
383 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
384 |
lemma continuous_on_cases_1: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
385 |
fixes s :: "real set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
386 |
assumes "continuous_on {t \<in> s. t \<le> a} f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
387 |
and "continuous_on {t \<in> s. a \<le> t} g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
388 |
and "a \<in> s \<Longrightarrow> f a = g a" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
389 |
shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
390 |
using assms |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
391 |
by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
392 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
393 |
|
70136 | 394 |
subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
395 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
396 |
lemma continuous_on_inverse_open_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
397 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
398 |
and imf: "f ` S = T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
399 |
and injf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
400 |
and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
401 |
shows "continuous_on T g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
402 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
403 |
from imf injf have gTS: "g ` T = S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
404 |
by force |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
405 |
from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
406 |
by force |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
407 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
408 |
by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
409 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
410 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
411 |
lemma continuous_on_inverse_closed_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
412 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
413 |
and imf: "f ` S = T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
414 |
and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
415 |
and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
416 |
shows "continuous_on T g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
417 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
418 |
from imf injf have gTS: "g ` T = S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
419 |
by force |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
420 |
from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
421 |
by force |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
422 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
423 |
by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
424 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
425 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
426 |
lemma homeomorphism_injective_open_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
427 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
428 |
and imf: "f ` S = T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
429 |
and injf: "inj_on f S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
430 |
and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
431 |
obtains g where "homeomorphism S T f g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
432 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
433 |
have "continuous_on T (inv_into S f)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
434 |
by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
435 |
with imf injf contf show "homeomorphism S T f (inv_into S f)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
436 |
by (auto simp: homeomorphism_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
437 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
438 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
439 |
lemma homeomorphism_injective_closed_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
440 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
441 |
and imf: "f ` S = T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
442 |
and injf: "inj_on f S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
443 |
and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
444 |
obtains g where "homeomorphism S T f g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
445 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
446 |
have "continuous_on T (inv_into S f)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
447 |
by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
448 |
with imf injf contf show "homeomorphism S T f (inv_into S f)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
449 |
by (auto simp: homeomorphism_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
450 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
451 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
452 |
lemma homeomorphism_imp_open_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
453 |
assumes hom: "homeomorphism S T f g" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
454 |
and oo: "openin (top_of_set S) U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
455 |
shows "openin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
456 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
457 |
from hom oo have [simp]: "f ` U = T \<inter> g -` U" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
458 |
using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
459 |
from hom have "continuous_on T g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
460 |
unfolding homeomorphism_def by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
461 |
moreover have "g ` T = S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
462 |
by (metis hom homeomorphism_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
463 |
ultimately show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
464 |
by (simp add: continuous_on_open oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
465 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
466 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
467 |
lemma homeomorphism_imp_closed_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
468 |
assumes hom: "homeomorphism S T f g" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
469 |
and oo: "closedin (top_of_set S) U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
470 |
shows "closedin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
471 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
472 |
from hom oo have [simp]: "f ` U = T \<inter> g -` U" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
473 |
using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
474 |
from hom have "continuous_on T g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
475 |
unfolding homeomorphism_def by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
476 |
moreover have "g ` T = S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
477 |
by (metis hom homeomorphism_def) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
478 |
ultimately show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
479 |
by (simp add: continuous_on_closed oo) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
480 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
481 |
|
70136 | 482 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Seperability\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
483 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
484 |
lemma subset_second_countable: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
485 |
obtains \<B> :: "'a:: second_countable_topology set set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
486 |
where "countable \<B>" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
487 |
"{} \<notin> \<B>" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
488 |
"\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
489 |
"\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
490 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
491 |
obtain \<B> :: "'a set set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
492 |
where "countable \<B>" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
493 |
and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
494 |
and \<B>: "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
495 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
496 |
obtain \<C> :: "'a set set" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
497 |
where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
498 |
and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
499 |
by (metis univ_second_countable that) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
500 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
501 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
502 |
show "countable ((\<lambda>C. S \<inter> C) ` \<C>)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
503 |
by (simp add: \<open>countable \<C>\<close>) |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
504 |
show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (top_of_set S) C" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
505 |
using ope by auto |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
506 |
show "\<And>T. openin (top_of_set S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
507 |
by (metis \<C> image_mono inf_Sup openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
508 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
509 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
510 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
511 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
512 |
show "countable (\<B> - {{}})" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
513 |
using \<open>countable \<B>\<close> by blast |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
514 |
show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (top_of_set S) C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
515 |
by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (top_of_set S) C\<close>) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
516 |
show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (top_of_set S) T" for T |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
517 |
using \<B> [OF that] |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
518 |
apply clarify |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
519 |
apply (rule_tac x="\<U> - {{}}" in exI, auto) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
520 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
521 |
qed auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
522 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
523 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
524 |
lemma Lindelof_openin: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
525 |
fixes \<F> :: "'a::second_countable_topology set set" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
526 |
assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set U) S" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
527 |
obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
528 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
529 |
have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
530 |
using assms by (simp add: openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
531 |
then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
532 |
by metis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
533 |
have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
534 |
using tf by fastforce |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
535 |
obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
536 |
using tf by (force intro: Lindelof [of "tf ` \<F>"]) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
537 |
then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
538 |
by (clarsimp simp add: countable_subset_image) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
539 |
then show ?thesis .. |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
540 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
541 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
542 |
|
70136 | 543 |
subsection\<^marker>\<open>tag unimportant\<close>\<open>Closed Maps\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
544 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
545 |
lemma continuous_imp_closed_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
546 |
fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
547 |
assumes "closedin (top_of_set S) U" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
548 |
"continuous_on S f" "f ` S = T" "compact S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
549 |
shows "closedin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
550 |
by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
551 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
552 |
lemma closed_map_restrict: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
553 |
assumes cloU: "closedin (top_of_set (S \<inter> f -` T')) U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
554 |
and cc: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
555 |
and "T' \<subseteq> T" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
556 |
shows "closedin (top_of_set T') (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
557 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
558 |
obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
559 |
using cloU by (auto simp: closedin_closed) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
560 |
with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
561 |
by (fastforce simp add: closedin_closed) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
562 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
563 |
|
70136 | 564 |
subsection\<^marker>\<open>tag unimportant\<close>\<open>Open Maps\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
565 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
566 |
lemma open_map_restrict: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
567 |
assumes opeU: "openin (top_of_set (S \<inter> f -` T')) U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
568 |
and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
569 |
and "T' \<subseteq> T" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
570 |
shows "openin (top_of_set T') (f ` U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
571 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
572 |
obtain V where "open V" "U = S \<inter> f -` T' \<inter> V" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
573 |
using opeU by (auto simp: openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
574 |
with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
575 |
by (fastforce simp add: openin_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
576 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
577 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
578 |
|
70136 | 579 |
subsection\<^marker>\<open>tag unimportant\<close>\<open>Quotient maps\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
580 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
581 |
lemma quotient_map_imp_continuous_open: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
582 |
assumes T: "f ` S \<subseteq> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
583 |
and ope: "\<And>U. U \<subseteq> T |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
584 |
\<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
585 |
openin (top_of_set T) U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
586 |
shows "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
587 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
588 |
have [simp]: "S \<inter> f -` f ` S = S" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
589 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
590 |
using ope [OF T] |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
591 |
apply (simp add: continuous_on_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
592 |
by (meson ope openin_imp_subset openin_trans) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
593 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
594 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
595 |
lemma quotient_map_imp_continuous_closed: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
596 |
assumes T: "f ` S \<subseteq> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
597 |
and ope: "\<And>U. U \<subseteq> T |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
598 |
\<Longrightarrow> (closedin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
599 |
closedin (top_of_set T) U)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
600 |
shows "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
601 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
602 |
have [simp]: "S \<inter> f -` f ` S = S" by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
603 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
604 |
using ope [OF T] |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
605 |
apply (simp add: continuous_on_closed) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
606 |
by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
607 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
608 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
609 |
lemma open_map_imp_quotient_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
610 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
611 |
and T: "T \<subseteq> f ` S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
612 |
and ope: "\<And>T. openin (top_of_set S) T |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
613 |
\<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
614 |
shows "openin (top_of_set S) (S \<inter> f -` T) = |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
615 |
openin (top_of_set (f ` S)) T" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
616 |
proof - |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
617 |
have "T = f ` (S \<inter> f -` T)" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
618 |
using T by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
619 |
then show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
620 |
using "ope" contf continuous_on_open by metis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
621 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
622 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
623 |
lemma closed_map_imp_quotient_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
624 |
assumes contf: "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
625 |
and T: "T \<subseteq> f ` S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
626 |
and ope: "\<And>T. closedin (top_of_set S) T |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
627 |
\<Longrightarrow> closedin (top_of_set (f ` S)) (f ` T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
628 |
shows "openin (top_of_set S) (S \<inter> f -` T) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
629 |
openin (top_of_set (f ` S)) T" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
630 |
(is "?lhs = ?rhs") |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
631 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
632 |
assume ?lhs |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
633 |
then have *: "closedin (top_of_set S) (S - (S \<inter> f -` T))" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
634 |
using closedin_diff by fastforce |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
635 |
have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
636 |
using T by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
637 |
show ?rhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
638 |
using ope [OF *, unfolded closedin_def] by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
639 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
640 |
assume ?rhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
641 |
with contf show ?lhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
642 |
by (auto simp: continuous_on_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
643 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
644 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
645 |
lemma continuous_right_inverse_imp_quotient_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
646 |
assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
647 |
and contg: "continuous_on T g" and img: "g ` T \<subseteq> S" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
648 |
and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
649 |
and U: "U \<subseteq> T" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
650 |
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
651 |
openin (top_of_set T) U" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
652 |
(is "?lhs = ?rhs") |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
653 |
proof - |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
654 |
have f: "\<And>Z. openin (top_of_set (f ` S)) Z \<Longrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
655 |
openin (top_of_set S) (S \<inter> f -` Z)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
656 |
and g: "\<And>Z. openin (top_of_set (g ` T)) Z \<Longrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
657 |
openin (top_of_set T) (T \<inter> g -` Z)" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
658 |
using contf contg by (auto simp: continuous_on_open) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
659 |
show ?thesis |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
660 |
proof |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
661 |
have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
662 |
using imf img by blast |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
663 |
also have "... = U" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
664 |
using U by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
665 |
finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" . |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
666 |
assume ?lhs |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
667 |
then have *: "openin (top_of_set (g ` T)) (g ` T \<inter> (S \<inter> f -` U))" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
668 |
by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
669 |
show ?rhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
670 |
using g [OF *] eq by auto |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
671 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
672 |
assume rhs: ?rhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
673 |
show ?lhs |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
674 |
by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
675 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
676 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
677 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
678 |
lemma continuous_left_inverse_imp_quotient_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
679 |
assumes "continuous_on S f" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
680 |
and "continuous_on (f ` S) g" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
681 |
and "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
682 |
and "U \<subseteq> f ` S" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
683 |
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
684 |
openin (top_of_set (f ` S)) U" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
685 |
apply (rule continuous_right_inverse_imp_quotient_map) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
686 |
using assms apply force+ |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
687 |
done |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
688 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
689 |
lemma continuous_imp_quotient_map: |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
690 |
fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
691 |
assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T" |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
692 |
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
693 |
openin (top_of_set T) U" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
694 |
by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
695 |
|
70136 | 696 |
subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
697 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
698 |
subsubsection\<open>on open sets\<close> |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
699 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
700 |
lemma pasting_lemma: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
701 |
assumes ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
702 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
703 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
704 |
and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
705 |
shows "continuous_map X Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
706 |
unfolding continuous_map_openin_preimage_eq |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
707 |
proof (intro conjI allI impI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
708 |
show "g ` topspace X \<subseteq> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
709 |
using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
710 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
711 |
fix U |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
712 |
assume Y: "openin Y U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
713 |
have T: "T i \<subseteq> topspace X" if "i \<in> I" for i |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
714 |
using ope by (simp add: openin_subset that) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
715 |
have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
716 |
using f g T by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
717 |
have "\<And>i. i \<in> I \<Longrightarrow> openin X (T i \<inter> f i -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
718 |
using cont unfolding continuous_map_openin_preimage_eq |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
719 |
by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
720 |
then show "openin X (topspace X \<inter> g -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
721 |
by (auto simp: *) |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
722 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
723 |
|
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
724 |
lemma pasting_lemma_exists: |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
725 |
assumes X: "topspace X \<subseteq> (\<Union>i \<in> I. T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
726 |
and ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
727 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
728 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
729 |
obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
730 |
proof |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
731 |
let ?h = "\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
732 |
show "continuous_map X Y ?h" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
733 |
apply (rule pasting_lemma [OF ope cont]) |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
734 |
apply (blast intro: f)+ |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
735 |
by (metis (no_types, lifting) UN_E X subsetD someI_ex) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
736 |
show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x" if "i \<in> I" "x \<in> topspace X \<inter> T i" for i x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
737 |
by (metis (no_types, lifting) IntD2 IntI f someI_ex that) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
738 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
739 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
740 |
lemma pasting_lemma_locally_finite: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
741 |
assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
742 |
and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
743 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
744 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
745 |
and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
746 |
shows "continuous_map X Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
747 |
unfolding continuous_map_closedin_preimage_eq |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
748 |
proof (intro conjI allI impI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
749 |
show "g ` topspace X \<subseteq> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
750 |
using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
751 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
752 |
fix U |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
753 |
assume Y: "closedin Y U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
754 |
have T: "T i \<subseteq> topspace X" if "i \<in> I" for i |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
755 |
using clo by (simp add: closedin_subset that) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
756 |
have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
757 |
using f g T by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
758 |
have cTf: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i \<inter> f i -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
759 |
using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
760 |
by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
761 |
have sub: "{Z \<in> (\<lambda>i. T i \<inter> f i -` U) ` I. Z \<inter> V \<noteq> {}} |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
762 |
\<subseteq> (\<lambda>i. T i \<inter> f i -` U) ` {i \<in> I. T i \<inter> V \<noteq> {}}" for V |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
763 |
by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
764 |
have 1: "(\<Union>i\<in>I. T i \<inter> f i -` U) \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
765 |
using T by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
766 |
then have lf: "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
767 |
unfolding locally_finite_in_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
768 |
using finite_subset [OF sub] fin by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
769 |
show "closedin X (topspace X \<inter> g -` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
770 |
apply (subst *) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
771 |
apply (rule closedin_locally_finite_Union) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
772 |
apply (auto intro: cTf lf) |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
773 |
done |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
774 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
775 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
776 |
subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
777 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
778 |
lemma pasting_lemma_closed: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
779 |
assumes fin: "finite I" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
780 |
and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
781 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
782 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
783 |
and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
784 |
shows "continuous_map X Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
785 |
using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
786 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
787 |
lemma pasting_lemma_exists_locally_finite: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
788 |
assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
789 |
and X: "topspace X \<subseteq> \<Union>(T ` I)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
790 |
and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
791 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
792 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
793 |
and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
794 |
obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
795 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
796 |
show "continuous_map X Y (\<lambda>x. f(@i. i \<in> I \<and> x \<in> T i) x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
797 |
apply (rule pasting_lemma_locally_finite [OF fin]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
798 |
apply (blast intro: assms)+ |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
799 |
by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex) |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
800 |
next |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
801 |
fix x i |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
802 |
assume "i \<in> I" and "x \<in> topspace X \<inter> T i" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
803 |
show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
804 |
apply (rule someI2_ex) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
805 |
using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
806 |
by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
807 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
808 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
809 |
lemma pasting_lemma_exists_closed: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
810 |
assumes fin: "finite I" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
811 |
and X: "topspace X \<subseteq> \<Union>(T ` I)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
812 |
and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
813 |
and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
814 |
and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
815 |
obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
816 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
817 |
show "continuous_map X Y (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
818 |
apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
819 |
apply (blast intro: f)+ |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
820 |
by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
821 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
822 |
fix x i |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
823 |
assume "i \<in> I" "x \<in> topspace X \<inter> T i" |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
824 |
then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x" |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
825 |
by (metis (no_types, lifting) IntD2 IntI f someI_ex) |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
826 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
827 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
828 |
lemma continuous_map_cases: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
829 |
assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
830 |
and g: "continuous_map (subtopology X (X closure_of {x. \<not> P x})) Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
831 |
and fg: "\<And>x. x \<in> X frontier_of {x. P x} \<Longrightarrow> f x = g x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
832 |
shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
833 |
proof (rule pasting_lemma_closed) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
834 |
let ?f = "\<lambda>b. if b then f else g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
835 |
let ?g = "\<lambda>x. if P x then f x else g x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
836 |
let ?T = "\<lambda>b. if b then X closure_of {x. P x} else X closure_of {x. ~P x}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
837 |
show "finite {True,False}" by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
838 |
have eq: "topspace X - Collect P = topspace X \<inter> {x. \<not> P x}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
839 |
by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
840 |
show "?f i x = ?f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
841 |
if "i \<in> {True,False}" "j \<in> {True,False}" and x: "x \<in> topspace X \<inter> ?T i \<inter> ?T j" for i j x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
842 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
843 |
have "f x = g x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
844 |
if "i" "\<not> j" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
845 |
apply (rule fg) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
846 |
unfolding frontier_of_closures eq |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
847 |
using x that closure_of_restrict by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
848 |
moreover |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
849 |
have "g x = f x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
850 |
if "x \<in> X closure_of {x. \<not> P x}" "x \<in> X closure_of Collect P" "\<not> i" "j" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
851 |
apply (rule fg [symmetric]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
852 |
unfolding frontier_of_closures eq |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
853 |
using x that closure_of_restrict by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
854 |
ultimately show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
855 |
using that by (auto simp flip: closure_of_restrict) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
856 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
857 |
show "\<exists>j. j \<in> {True,False} \<and> x \<in> ?T j \<and> (if P x then f x else g x) = ?f j x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
858 |
if "x \<in> topspace X" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
859 |
apply simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
860 |
apply safe |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
861 |
apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
862 |
by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
863 |
qed (auto simp: f g) |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
864 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
865 |
lemma continuous_map_cases_alt: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
866 |
assumes f: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. P x})) Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
867 |
and g: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. ~P x})) Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
868 |
and fg: "\<And>x. x \<in> X frontier_of {x \<in> topspace X. P x} \<Longrightarrow> f x = g x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
869 |
shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
870 |
apply (rule continuous_map_cases) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
871 |
using assms |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
872 |
apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
873 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
874 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
875 |
lemma continuous_map_cases_function: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
876 |
assumes contp: "continuous_map X Z p" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
877 |
and contf: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of U}) Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
878 |
and contg: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}) Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
879 |
and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x \<in> Z frontier_of U\<rbrakk> \<Longrightarrow> f x = g x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
880 |
shows "continuous_map X Y (\<lambda>x. if p x \<in> U then f x else g x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
881 |
proof (rule continuous_map_cases_alt) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
882 |
show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<in> U})) Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
883 |
proof (rule continuous_map_from_subtopology_mono) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
884 |
let ?T = "{x \<in> topspace X. p x \<in> Z closure_of U}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
885 |
show "continuous_map (subtopology X ?T) Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
886 |
by (simp add: contf) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
887 |
show "X closure_of {x \<in> topspace X. p x \<in> U} \<subseteq> ?T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
888 |
by (rule continuous_map_closure_preimage_subset [OF contp]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
889 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
890 |
show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<notin> U})) Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
891 |
proof (rule continuous_map_from_subtopology_mono) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
892 |
let ?T = "{x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
893 |
show "continuous_map (subtopology X ?T) Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
894 |
by (simp add: contg) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
895 |
have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
896 |
apply (rule closure_of_mono) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
897 |
using continuous_map_closedin contp by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
898 |
then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
899 |
by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
900 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
901 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
902 |
show "f x = g x" if "x \<in> X frontier_of {x \<in> topspace X. p x \<in> U}" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
903 |
using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast |
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
904 |
qed |
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
905 |
|
69750 | 906 |
subsection \<open>Retractions\<close> |
907 |
||
70136 | 908 |
definition\<^marker>\<open>tag important\<close> retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
69750 | 909 |
where "retraction S T r \<longleftrightarrow> |
910 |
T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)" |
|
911 |
||
70136 | 912 |
definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where |
69750 | 913 |
"T retract_of S \<longleftrightarrow> (\<exists>r. retraction S T r)" |
914 |
||
915 |
lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow> r (r x) = r x" |
|
916 |
unfolding retraction_def by auto |
|
917 |
||
918 |
text \<open>Preservation of fixpoints under (more general notion of) retraction\<close> |
|
919 |
||
920 |
lemma invertible_fixpoint_property: |
|
921 |
fixes S :: "'a::topological_space set" |
|
922 |
and T :: "'b::topological_space set" |
|
923 |
assumes contt: "continuous_on T i" |
|
924 |
and "i ` T \<subseteq> S" |
|
925 |
and contr: "continuous_on S r" |
|
926 |
and "r ` S \<subseteq> T" |
|
927 |
and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y" |
|
928 |
and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x" |
|
929 |
and contg: "continuous_on T g" |
|
930 |
and "g ` T \<subseteq> T" |
|
931 |
obtains y where "y \<in> T" and "g y = y" |
|
932 |
proof - |
|
933 |
have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x" |
|
934 |
proof (rule FP) |
|
935 |
show "continuous_on S (i \<circ> g \<circ> r)" |
|
936 |
by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset) |
|
937 |
show "(i \<circ> g \<circ> r) ` S \<subseteq> S" |
|
938 |
using assms(2,4,8) by force |
|
939 |
qed |
|
940 |
then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" .. |
|
941 |
then have *: "g (r x) \<in> T" |
|
942 |
using assms(4,8) by auto |
|
943 |
have "r ((i \<circ> g \<circ> r) x) = r x" |
|
944 |
using x by auto |
|
945 |
then show ?thesis |
|
946 |
using "*" ri that by auto |
|
947 |
qed |
|
948 |
||
949 |
lemma homeomorphic_fixpoint_property: |
|
950 |
fixes S :: "'a::topological_space set" |
|
951 |
and T :: "'b::topological_space set" |
|
952 |
assumes "S homeomorphic T" |
|
953 |
shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow> |
|
954 |
(\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))" |
|
955 |
(is "?lhs = ?rhs") |
|
956 |
proof - |
|
957 |
obtain r i where r: |
|
958 |
"\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r" |
|
959 |
"\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i" |
|
960 |
using assms unfolding homeomorphic_def homeomorphism_def by blast |
|
961 |
show ?thesis |
|
962 |
proof |
|
963 |
assume ?lhs |
|
964 |
with r show ?rhs |
|
965 |
by (metis invertible_fixpoint_property[of T i S r] order_refl) |
|
966 |
next |
|
967 |
assume ?rhs |
|
968 |
with r show ?lhs |
|
969 |
by (metis invertible_fixpoint_property[of S r T i] order_refl) |
|
970 |
qed |
|
971 |
qed |
|
972 |
||
973 |
lemma retract_fixpoint_property: |
|
974 |
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
|
975 |
and S :: "'a set" |
|
976 |
assumes "T retract_of S" |
|
977 |
and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x" |
|
978 |
and contg: "continuous_on T g" |
|
979 |
and "g ` T \<subseteq> T" |
|
980 |
obtains y where "y \<in> T" and "g y = y" |
|
981 |
proof - |
|
982 |
obtain h where "retraction S T h" |
|
983 |
using assms(1) unfolding retract_of_def .. |
|
984 |
then show ?thesis |
|
985 |
unfolding retraction_def |
|
986 |
using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP] |
|
987 |
by (metis assms(4) contg image_ident that) |
|
988 |
qed |
|
989 |
||
990 |
lemma retraction: |
|
991 |
"retraction S T r \<longleftrightarrow> |
|
992 |
T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)" |
|
993 |
by (force simp: retraction_def) |
|
994 |
||
69753 | 995 |
lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close> |
69750 | 996 |
assumes "retraction S T r" |
997 |
obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x" |
|
998 |
proof (rule that) |
|
999 |
from retraction [of S T r] assms |
|
1000 |
have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x" |
|
1001 |
by simp_all |
|
1002 |
then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" |
|
1003 |
by simp_all |
|
1004 |
from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x |
|
1005 |
using that by simp |
|
1006 |
with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x |
|
1007 |
using that by auto |
|
1008 |
qed |
|
1009 |
||
69753 | 1010 |
lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close> |
69750 | 1011 |
assumes "T retract_of S" |
1012 |
obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x" |
|
1013 |
proof - |
|
1014 |
from assms obtain r where "retraction S T r" |
|
1015 |
by (auto simp add: retract_of_def) |
|
1016 |
with that show thesis |
|
1017 |
by (auto elim: retractionE) |
|
1018 |
qed |
|
1019 |
||
1020 |
lemma retract_of_imp_extensible: |
|
1021 |
assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U" |
|
1022 |
obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
1023 |
proof - |
|
1024 |
from \<open>S retract_of T\<close> obtain r where "retraction T S r" |
|
1025 |
by (auto simp add: retract_of_def) |
|
1026 |
show thesis |
|
1027 |
by (rule that [of "f \<circ> r"]) |
|
1028 |
(use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>) |
|
1029 |
qed |
|
1030 |
||
1031 |
lemma idempotent_imp_retraction: |
|
1032 |
assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x" |
|
1033 |
shows "retraction S (f ` S) f" |
|
1034 |
by (simp add: assms retraction) |
|
1035 |
||
1036 |
lemma retraction_subset: |
|
1037 |
assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S" |
|
1038 |
shows "retraction s' T r" |
|
1039 |
unfolding retraction_def |
|
1040 |
by (metis assms continuous_on_subset image_mono retraction) |
|
1041 |
||
1042 |
lemma retract_of_subset: |
|
1043 |
assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S" |
|
1044 |
shows "T retract_of s'" |
|
1045 |
by (meson assms retract_of_def retraction_subset) |
|
1046 |
||
1047 |
lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)" |
|
1048 |
by (simp add: retraction) |
|
1049 |
||
1050 |
lemma retract_of_refl [iff]: "S retract_of S" |
|
1051 |
unfolding retract_of_def retraction_def |
|
1052 |
using continuous_on_id by blast |
|
1053 |
||
1054 |
lemma retract_of_imp_subset: |
|
1055 |
"S retract_of T \<Longrightarrow> S \<subseteq> T" |
|
1056 |
by (simp add: retract_of_def retraction_def) |
|
1057 |
||
1058 |
lemma retract_of_empty [simp]: |
|
1059 |
"({} retract_of S) \<longleftrightarrow> S = {}" "(S retract_of {}) \<longleftrightarrow> S = {}" |
|
1060 |
by (auto simp: retract_of_def retraction_def) |
|
1061 |
||
1062 |
lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S" |
|
1063 |
unfolding retract_of_def retraction_def by force |
|
1064 |
||
1065 |
lemma retraction_comp: |
|
1066 |
"\<lbrakk>retraction S T f; retraction T U g\<rbrakk> |
|
1067 |
\<Longrightarrow> retraction S U (g \<circ> f)" |
|
1068 |
apply (auto simp: retraction_def intro: continuous_on_compose2) |
|
1069 |
by blast |
|
1070 |
||
1071 |
lemma retract_of_trans [trans]: |
|
1072 |
assumes "S retract_of T" and "T retract_of U" |
|
1073 |
shows "S retract_of U" |
|
1074 |
using assms by (auto simp: retract_of_def intro: retraction_comp) |
|
1075 |
||
1076 |
lemma closedin_retract: |
|
1077 |
fixes S :: "'a :: t2_space set" |
|
1078 |
assumes "S retract_of T" |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1079 |
shows "closedin (top_of_set T) S" |
69750 | 1080 |
proof - |
1081 |
obtain r where r: "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x" |
|
1082 |
using assms by (auto simp: retract_of_def retraction_def) |
|
1083 |
have "S = {x\<in>T. x = r x}" |
|
1084 |
using r by auto |
|
1085 |
also have "\<dots> = T \<inter> ((\<lambda>x. (x, r x)) -` ({y. \<exists>x. y = (x, x)}))" |
|
1086 |
unfolding vimage_def mem_Times_iff fst_conv snd_conv |
|
1087 |
using r |
|
1088 |
by auto |
|
1089 |
also have "closedin (top_of_set T) \<dots>" |
|
1090 |
by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r) |
|
1091 |
finally show ?thesis . |
|
1092 |
qed |
|
1093 |
||
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1094 |
lemma closedin_self [simp]: "closedin (top_of_set S) S" |
69750 | 1095 |
by simp |
1096 |
||
1097 |
lemma retract_of_closed: |
|
1098 |
fixes S :: "'a :: t2_space set" |
|
1099 |
shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S" |
|
1100 |
by (metis closedin_retract closedin_closed_eq) |
|
1101 |
||
1102 |
lemma retract_of_compact: |
|
1103 |
"\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S" |
|
1104 |
by (metis compact_continuous_image retract_of_def retraction) |
|
1105 |
||
1106 |
lemma retract_of_connected: |
|
1107 |
"\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S" |
|
1108 |
by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction) |
|
1109 |
||
1110 |
lemma retraction_imp_quotient_map: |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1111 |
"openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" |
69750 | 1112 |
if retraction: "retraction S T r" and "U \<subseteq> T" |
1113 |
using retraction apply (rule retractionE) |
|
1114 |
apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) |
|
1115 |
using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset) |
|
1116 |
done |
|
1117 |
||
1118 |
lemma retract_of_Times: |
|
1119 |
"\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')" |
|
1120 |
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify) |
|
1121 |
apply (rename_tac f g) |
|
1122 |
apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI) |
|
1123 |
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+ |
|
1124 |
done |
|
1125 |
||
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1126 |
subsection\<open>Retractions on a topological space\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1127 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1128 |
definition retract_of_space :: "'a set \<Rightarrow> 'a topology \<Rightarrow> bool" (infix "retract'_of'_space" 50) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1129 |
where "S retract_of_space X |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1130 |
\<equiv> S \<subseteq> topspace X \<and> (\<exists>r. continuous_map X (subtopology X S) r \<and> (\<forall>x \<in> S. r x = x))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1131 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1132 |
lemma retract_of_space_retraction_maps: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1133 |
"S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<exists>r. retraction_maps X (subtopology X S) r id)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1134 |
by (auto simp: retract_of_space_def retraction_maps_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1135 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1136 |
lemma retract_of_space_section_map: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1137 |
"S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> section_map (subtopology X S) X id" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1138 |
unfolding retract_of_space_def retraction_maps_def section_map_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1139 |
by (auto simp: continuous_map_from_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1140 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1141 |
lemma retract_of_space_imp_subset: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1142 |
"S retract_of_space X \<Longrightarrow> S \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1143 |
by (simp add: retract_of_space_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1144 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1145 |
lemma retract_of_space_topspace: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1146 |
"topspace X retract_of_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1147 |
using retract_of_space_def by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1148 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1149 |
lemma retract_of_space_empty [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1150 |
"{} retract_of_space X \<longleftrightarrow> topspace X = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1151 |
by (auto simp: continuous_map_def retract_of_space_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1152 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1153 |
lemma retract_of_space_singleton [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1154 |
"{a} retract_of_space X \<longleftrightarrow> a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1155 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1156 |
have "continuous_map X (subtopology X {a}) (\<lambda>x. a) \<and> (\<lambda>x. a) a = a" if "a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1157 |
using that by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1158 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1159 |
by (force simp: retract_of_space_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1160 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1161 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1162 |
lemma retract_of_space_clopen: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1163 |
assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1164 |
shows "S retract_of_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1165 |
proof (cases "S = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1166 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1167 |
then obtain a where "a \<in> S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1168 |
by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1169 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1170 |
unfolding retract_of_space_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1171 |
proof (intro exI conjI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1172 |
show "S \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1173 |
by (simp add: assms closedin_subset) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1174 |
have "continuous_map X X (\<lambda>x. if x \<in> S then x else a)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1175 |
proof (rule continuous_map_cases) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1176 |
show "continuous_map (subtopology X (X closure_of {x. x \<in> S})) X (\<lambda>x. x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1177 |
by (simp add: continuous_map_from_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1178 |
show "continuous_map (subtopology X (X closure_of {x. x \<notin> S})) X (\<lambda>x. a)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1179 |
using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1180 |
show "x = a" if "x \<in> X frontier_of {x. x \<in> S}" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1181 |
using assms that clopenin_eq_frontier_of by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1182 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1183 |
then show "continuous_map X (subtopology X S) (\<lambda>x. if x \<in> S then x else a)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1184 |
using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> by (auto simp: continuous_map_in_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1185 |
qed auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1186 |
qed (use assms in auto) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1187 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1188 |
lemma retract_of_space_disjoint_union: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1189 |
assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \<union> T = topspace X" and "S = {} \<Longrightarrow> topspace X = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1190 |
shows "S retract_of_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1191 |
proof (rule retract_of_space_clopen) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1192 |
have "S \<inter> T = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1193 |
by (meson ST disjnt_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1194 |
then have "S = topspace X - T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1195 |
using ST by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1196 |
then show "closedin X S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1197 |
using \<open>openin X T\<close> by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1198 |
qed (auto simp: assms) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1199 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1200 |
lemma retraction_maps_section_image1: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1201 |
assumes "retraction_maps X Y r s" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1202 |
shows "s ` (topspace Y) retract_of_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1203 |
unfolding retract_of_space_section_map |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1204 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1205 |
show "s ` topspace Y \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1206 |
using assms continuous_map_image_subset_topspace retraction_maps_def by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1207 |
show "section_map (subtopology X (s ` topspace Y)) X id" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1208 |
unfolding section_map_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1209 |
using assms retraction_maps_to_retract_maps by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1210 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1211 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1212 |
lemma retraction_maps_section_image2: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1213 |
"retraction_maps X Y r s |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1214 |
\<Longrightarrow> subtopology X (s ` (topspace Y)) homeomorphic_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1215 |
using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1216 |
section_map_def by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1217 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1218 |
subsection\<open>Paths and path-connectedness\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1219 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1220 |
definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1221 |
"pathin X g \<equiv> continuous_map (subtopology euclideanreal {0..1}) X g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1222 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1223 |
lemma pathin_compose: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1224 |
"\<lbrakk>pathin X g; continuous_map X Y f\<rbrakk> \<Longrightarrow> pathin Y (f \<circ> g)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1225 |
by (simp add: continuous_map_compose pathin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1226 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1227 |
lemma pathin_subtopology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1228 |
"pathin (subtopology X S) g \<longleftrightarrow> pathin X g \<and> (\<forall>x \<in> {0..1}. g x \<in> S)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1229 |
by (auto simp: pathin_def continuous_map_in_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1230 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1231 |
lemma pathin_const: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1232 |
"pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1233 |
by (simp add: pathin_def) |
69939
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1234 |
|
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1235 |
lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> topspace X" |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1236 |
by (force simp: pathin_def continuous_map) |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1237 |
|
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1238 |
lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X" |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1239 |
by (force simp: pathin_def continuous_map) |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1240 |
|
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1241 |
lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X" |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1242 |
by (force simp: pathin_def continuous_map) |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1243 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1244 |
definition path_connected_space :: "'a topology \<Rightarrow> bool" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1245 |
where "path_connected_space X \<equiv> \<forall>x \<in> topspace X. \<forall> y \<in> topspace X. \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1246 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1247 |
definition path_connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1248 |
where "path_connectedin X S \<equiv> S \<subseteq> topspace X \<and> path_connected_space(subtopology X S)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1249 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1250 |
lemma path_connectedin_absolute [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1251 |
"path_connectedin (subtopology X S) S \<longleftrightarrow> path_connectedin X S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1252 |
by (simp add: path_connectedin_def subtopology_subtopology topspace_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1253 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1254 |
lemma path_connectedin_subset_topspace: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1255 |
"path_connectedin X S \<Longrightarrow> S \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1256 |
by (simp add: path_connectedin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1257 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1258 |
lemma path_connectedin_subtopology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1259 |
"path_connectedin (subtopology X S) T \<longleftrightarrow> path_connectedin X T \<and> T \<subseteq> S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1260 |
by (auto simp: path_connectedin_def subtopology_subtopology topspace_subtopology inf.absorb2) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1261 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1262 |
lemma path_connectedin: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1263 |
"path_connectedin X S \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1264 |
S \<subseteq> topspace X \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1265 |
(\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> g 1 = y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1266 |
unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1267 |
by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 topspace_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1268 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1269 |
lemma path_connectedin_topspace: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1270 |
"path_connectedin X (topspace X) \<longleftrightarrow> path_connected_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1271 |
by (simp add: path_connectedin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1272 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1273 |
lemma path_connected_imp_connected_space: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1274 |
assumes "path_connected_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1275 |
shows "connected_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1276 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1277 |
have *: "\<exists>S. connectedin X S \<and> g 0 \<in> S \<and> g 1 \<in> S" if "pathin X g" for g |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1278 |
proof (intro exI conjI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1279 |
have "continuous_map (subtopology euclideanreal {0..1}) X g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1280 |
using connectedin_absolute that by (simp add: pathin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1281 |
then show "connectedin X (g ` {0..1})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1282 |
by (rule connectedin_continuous_map_image) auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1283 |
qed auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1284 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1285 |
using assms |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1286 |
by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1287 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1288 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1289 |
lemma path_connectedin_imp_connectedin: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1290 |
"path_connectedin X S \<Longrightarrow> connectedin X S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1291 |
by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1292 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1293 |
lemma path_connected_space_topspace_empty: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1294 |
"topspace X = {} \<Longrightarrow> path_connected_space X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1295 |
by (simp add: path_connected_space_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1296 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1297 |
lemma path_connectedin_empty [simp]: "path_connectedin X {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1298 |
by (simp add: path_connectedin) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1299 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1300 |
lemma path_connectedin_singleton [simp]: "path_connectedin X {a} \<longleftrightarrow> a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1301 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1302 |
show "path_connectedin X {a} \<Longrightarrow> a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1303 |
by (simp add: path_connectedin) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1304 |
show "a \<in> topspace X \<Longrightarrow> path_connectedin X {a}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1305 |
unfolding path_connectedin |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1306 |
using pathin_const by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1307 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1308 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1309 |
lemma path_connectedin_continuous_map_image: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1310 |
assumes f: "continuous_map X Y f" and S: "path_connectedin X S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1311 |
shows "path_connectedin Y (f ` S)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1312 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1313 |
have fX: "f ` (topspace X) \<subseteq> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1314 |
by (metis f continuous_map_image_subset_topspace) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1315 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1316 |
unfolding path_connectedin |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1317 |
proof (intro conjI ballI; clarify?) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1318 |
fix x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1319 |
assume "x \<in> S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1320 |
show "f x \<in> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1321 |
by (meson S fX \<open>x \<in> S\<close> image_subset_iff path_connectedin_subset_topspace set_mp) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1322 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1323 |
fix x y |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1324 |
assume "x \<in> S" and "y \<in> S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1325 |
then obtain g where g: "pathin X g" "g ` {0..1} \<subseteq> S" "g 0 = x" "g 1 = y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1326 |
using S by (force simp: path_connectedin) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1327 |
show "\<exists>g. pathin Y g \<and> g ` {0..1} \<subseteq> f ` S \<and> g 0 = f x \<and> g 1 = f y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1328 |
proof (intro exI conjI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1329 |
show "pathin Y (f \<circ> g)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1330 |
using \<open>pathin X g\<close> f pathin_compose by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1331 |
qed (use g in auto) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1332 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1333 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1334 |
|
69939
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1335 |
lemma path_connectedin_discrete_topology: |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1336 |
"path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})" |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1337 |
apply safe |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1338 |
using path_connectedin_subset_topspace apply fastforce |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1339 |
apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin) |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1340 |
using subset_singletonD by fastforce |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1341 |
|
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1342 |
lemma path_connected_space_discrete_topology: |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1343 |
"path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})" |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1344 |
by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1345 |
subset_singletonD topspace_discrete_topology) |
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1346 |
|
812ce526da33
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset
|
1347 |
|
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1348 |
lemma homeomorphic_path_connected_space_imp: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1349 |
"\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1350 |
unfolding homeomorphic_space_def homeomorphic_maps_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1351 |
by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1352 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1353 |
lemma homeomorphic_path_connected_space: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1354 |
"X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1355 |
by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1356 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1357 |
lemma homeomorphic_map_path_connectedness: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1358 |
assumes "homeomorphic_map X Y f" "U \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1359 |
shows "path_connectedin Y (f ` U) \<longleftrightarrow> path_connectedin X U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1360 |
unfolding path_connectedin_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1361 |
proof (intro conj_cong homeomorphic_path_connected_space) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1362 |
show "(f ` U \<subseteq> topspace Y) = (U \<subseteq> topspace X)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1363 |
using assms homeomorphic_imp_surjective_map by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1364 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1365 |
assume "U \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1366 |
show "subtopology Y (f ` U) homeomorphic_space subtopology X U" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1367 |
using assms unfolding homeomorphic_eq_everything_map |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1368 |
by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1369 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1370 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1371 |
lemma homeomorphic_map_path_connectedness_eq: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1372 |
"homeomorphic_map X Y f \<Longrightarrow> path_connectedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> path_connectedin Y (f ` U)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1373 |
by (meson homeomorphic_map_path_connectedness path_connectedin_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1374 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1375 |
subsection\<open>Connected components\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1376 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1377 |
definition connected_component_of :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1378 |
where "connected_component_of X x y \<equiv> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1379 |
\<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1380 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1381 |
abbreviation connected_component_of_set |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1382 |
where "connected_component_of_set X x \<equiv> Collect (connected_component_of X x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1383 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1384 |
definition connected_components_of :: "'a topology \<Rightarrow> ('a set) set" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1385 |
where "connected_components_of X \<equiv> connected_component_of_set X ` topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1386 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1387 |
lemma connected_component_in_topspace: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1388 |
"connected_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1389 |
by (meson connected_component_of_def connectedin_subset_topspace in_mono) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1390 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1391 |
lemma connected_component_of_refl: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1392 |
"connected_component_of X x x \<longleftrightarrow> x \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1393 |
by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1394 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1395 |
lemma connected_component_of_sym: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1396 |
"connected_component_of X x y \<longleftrightarrow> connected_component_of X y x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1397 |
by (meson connected_component_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1398 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1399 |
lemma connected_component_of_trans: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1400 |
"\<lbrakk>connected_component_of X x y; connected_component_of X y z\<rbrakk> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1401 |
\<Longrightarrow> connected_component_of X x z" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1402 |
unfolding connected_component_of_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1403 |
using connectedin_Un by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1404 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1405 |
lemma connected_component_of_mono: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1406 |
"\<lbrakk>connected_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1407 |
\<Longrightarrow> connected_component_of (subtopology X T) x y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1408 |
by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1409 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1410 |
lemma connected_component_of_set: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1411 |
"connected_component_of_set X x = {y. \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1412 |
by (meson connected_component_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1413 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1414 |
lemma connected_component_of_subset_topspace: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1415 |
"connected_component_of_set X x \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1416 |
using connected_component_in_topspace by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1417 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1418 |
lemma connected_component_of_eq_empty: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1419 |
"connected_component_of_set X x = {} \<longleftrightarrow> (x \<notin> topspace X)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1420 |
using connected_component_in_topspace connected_component_of_refl by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1421 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1422 |
lemma connected_space_iff_connected_component: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1423 |
"connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. connected_component_of X x y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1424 |
by (simp add: connected_component_of_def connected_space_subconnected) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1425 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1426 |
lemma connected_space_imp_connected_component_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1427 |
"\<lbrakk>connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1428 |
\<Longrightarrow> connected_component_of X a b" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1429 |
by (simp add: connected_space_iff_connected_component) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1430 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1431 |
lemma connected_space_connected_component_set: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1432 |
"connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. connected_component_of_set X x = topspace X)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1433 |
using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1434 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1435 |
lemma connected_component_of_maximal: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1436 |
"\<lbrakk>connectedin X S; x \<in> S\<rbrakk> \<Longrightarrow> S \<subseteq> connected_component_of_set X x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1437 |
by (meson Ball_Collect connected_component_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1438 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1439 |
lemma connected_component_of_equiv: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1440 |
"connected_component_of X x y \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1441 |
x \<in> topspace X \<and> y \<in> topspace X \<and> connected_component_of X x = connected_component_of X y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1442 |
apply (simp add: connected_component_in_topspace fun_eq_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1443 |
by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1444 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1445 |
lemma connected_component_of_disjoint: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1446 |
"disjnt (connected_component_of_set X x) (connected_component_of_set X y) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1447 |
\<longleftrightarrow> ~(connected_component_of X x y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1448 |
using connected_component_of_equiv unfolding disjnt_iff by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1449 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1450 |
lemma connected_component_of_eq: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1451 |
"connected_component_of X x = connected_component_of X y \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1452 |
(x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1453 |
x \<in> topspace X \<and> y \<in> topspace X \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1454 |
connected_component_of X x y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1455 |
by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1456 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1457 |
lemma connectedin_connected_component_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1458 |
"connectedin X (connected_component_of_set X x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1459 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1460 |
have "connected_component_of_set X x = \<Union> {T. connectedin X T \<and> x \<in> T}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1461 |
by (auto simp: connected_component_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1462 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1463 |
apply (rule ssubst) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1464 |
by (blast intro: connectedin_Union) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1465 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1466 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1467 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1468 |
lemma Union_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1469 |
"\<Union>(connected_components_of X) = topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1470 |
unfolding connected_components_of_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1471 |
apply (rule equalityI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1472 |
apply (simp add: SUP_least connected_component_of_subset_topspace) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1473 |
using connected_component_of_refl by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1474 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1475 |
lemma connected_components_of_maximal: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1476 |
"\<lbrakk>C \<in> connected_components_of X; connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1477 |
unfolding connected_components_of_def disjnt_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1478 |
apply clarify |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1479 |
by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1480 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1481 |
lemma pairwise_disjoint_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1482 |
"pairwise disjnt (connected_components_of X)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1483 |
unfolding connected_components_of_def pairwise_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1484 |
apply clarify |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1485 |
by (metis connected_component_of_disjoint connected_component_of_equiv) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1486 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1487 |
lemma complement_connected_components_of_Union: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1488 |
"C \<in> connected_components_of X |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1489 |
\<Longrightarrow> topspace X - C = \<Union> (connected_components_of X - {C})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1490 |
apply (rule equalityI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1491 |
using Union_connected_components_of apply fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1492 |
by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1493 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1494 |
lemma nonempty_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1495 |
"C \<in> connected_components_of X \<Longrightarrow> C \<noteq> {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1496 |
unfolding connected_components_of_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1497 |
by (metis (no_types, lifting) connected_component_of_eq_empty imageE) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1498 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1499 |
lemma connected_components_of_subset: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1500 |
"C \<in> connected_components_of X \<Longrightarrow> C \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1501 |
using Union_connected_components_of by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1502 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1503 |
lemma connectedin_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1504 |
assumes "C \<in> connected_components_of X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1505 |
shows "connectedin X C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1506 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1507 |
have "C \<in> connected_component_of_set X ` topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1508 |
using assms connected_components_of_def by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1509 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1510 |
using connectedin_connected_component_of by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1511 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1512 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1513 |
lemma connected_component_in_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1514 |
"connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1515 |
apply (rule iffI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1516 |
using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1517 |
by (simp add: connected_components_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1518 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1519 |
lemma connected_space_iff_components_eq: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1520 |
"connected_space X \<longleftrightarrow> (\<forall>C \<in> connected_components_of X. \<forall>C' \<in> connected_components_of X. C = C')" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1521 |
apply (rule iffI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1522 |
apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1523 |
by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1524 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1525 |
lemma connected_components_of_eq_empty: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1526 |
"connected_components_of X = {} \<longleftrightarrow> topspace X = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1527 |
by (simp add: connected_components_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1528 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1529 |
lemma connected_components_of_empty_space: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1530 |
"topspace X = {} \<Longrightarrow> connected_components_of X = {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1531 |
by (simp add: connected_components_of_eq_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1532 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1533 |
lemma connected_components_of_subset_sing: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1534 |
"connected_components_of X \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (topspace X = {} \<or> topspace X = S)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1535 |
proof (cases "topspace X = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1536 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1537 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1538 |
by (simp add: connected_components_of_empty_space connected_space_topspace_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1539 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1540 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1541 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1542 |
by (metis (no_types, hide_lams) Union_connected_components_of ccpo_Sup_singleton |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1543 |
connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1544 |
subsetI subset_singleton_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1545 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1546 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1547 |
lemma connected_space_iff_components_subset_singleton: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1548 |
"connected_space X \<longleftrightarrow> (\<exists>a. connected_components_of X \<subseteq> {a})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1549 |
by (simp add: connected_components_of_subset_sing) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1550 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1551 |
lemma connected_components_of_eq_singleton: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1552 |
"connected_components_of X = {S} |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1553 |
\<longleftrightarrow> connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1554 |
by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1555 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1556 |
lemma connected_components_of_connected_space: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1557 |
"connected_space X \<Longrightarrow> connected_components_of X = (if topspace X = {} then {} else {topspace X})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1558 |
by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1559 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1560 |
lemma exists_connected_component_of_superset: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1561 |
assumes "connectedin X S" and ne: "topspace X \<noteq> {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1562 |
shows "\<exists>C. C \<in> connected_components_of X \<and> S \<subseteq> C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1563 |
proof (cases "S = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1564 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1565 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1566 |
using ne connected_components_of_def by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1567 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1568 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1569 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1570 |
by (meson all_not_in_conv assms(1) connected_component_in_connected_components_of connected_component_of_maximal connectedin_subset_topspace in_mono) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1571 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1572 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1573 |
lemma closedin_connected_components_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1574 |
assumes "C \<in> connected_components_of X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1575 |
shows "closedin X C" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1576 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1577 |
obtain x where "x \<in> topspace X" and x: "C = connected_component_of_set X x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1578 |
using assms by (auto simp: connected_components_of_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1579 |
have "connected_component_of_set X x \<subseteq> topspace X" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1580 |
by (simp add: connected_component_of_subset_topspace) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1581 |
moreover have "X closure_of connected_component_of_set X x \<subseteq> connected_component_of_set X x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1582 |
proof (rule connected_component_of_maximal) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1583 |
show "connectedin X (X closure_of connected_component_of_set X x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1584 |
by (simp add: connectedin_closure_of connectedin_connected_component_of) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1585 |
show "x \<in> X closure_of connected_component_of_set X x" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1586 |
by (simp add: \<open>x \<in> topspace X\<close> closure_of connected_component_of_refl) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1587 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1588 |
ultimately |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1589 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1590 |
using closure_of_subset_eq x by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1591 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1592 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1593 |
lemma closedin_connected_component_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1594 |
"closedin X (connected_component_of_set X x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1595 |
by (metis closedin_connected_components_of closedin_empty connected_component_in_connected_components_of connected_component_of_eq_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1596 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1597 |
lemma connected_component_of_eq_overlap: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1598 |
"connected_component_of_set X x = connected_component_of_set X y \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1599 |
(x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1600 |
~(connected_component_of_set X x \<inter> connected_component_of_set X y = {})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1601 |
using connected_component_of_equiv by fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1602 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1603 |
lemma connected_component_of_nonoverlap: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1604 |
"connected_component_of_set X x \<inter> connected_component_of_set X y = {} \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1605 |
(x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1606 |
~(connected_component_of_set X x = connected_component_of_set X y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1607 |
by (metis connected_component_of_eq_empty connected_component_of_eq_overlap inf.idem) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1608 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1609 |
lemma connected_component_of_overlap: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1610 |
"~(connected_component_of_set X x \<inter> connected_component_of_set X y = {}) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1611 |
x \<in> topspace X \<and> y \<in> topspace X \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1612 |
connected_component_of_set X x = connected_component_of_set X y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1613 |
by (meson connected_component_of_nonoverlap) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1614 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69753
diff
changeset
|
1615 |
|
69616
d18dc9c5c456
split off theory combining Elementary_Topology and Abstract_Topology
immler
parents:
diff
changeset
|
1616 |
end |