summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Topology_Euclidean_Space.thy

changeset 64911 | f0e07600de47 |

parent 64910 | 6108dddad9f0 |

child 65036 | ab7e11730ad8 |

1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 11:26:21 2017 +0100 1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 13:59:10 2017 +0100 1.3 @@ -499,9 +499,9 @@ 1.4 proof - 1.5 obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto 1.6 define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}" 1.7 - then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image) 1.8 + then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 1.9 define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}" 1.10 - then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image) 1.11 + then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 1.12 have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y 1.13 proof (cases) 1.14 assume "\<exists>z. x < z \<and> z < y" 1.15 @@ -509,27 +509,27 @@ 1.16 define U where "U = {x<..<y}" 1.17 then have "open U" by simp 1.18 moreover have "z \<in> U" using z U_def by simp 1.19 - ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto 1.20 + ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 1.21 define w where "w = (SOME x. x \<in> V)" 1.22 - then have "w \<in> V" using `z \<in> V` by (metis someI2) 1.23 - then have "x < w \<and> w \<le> y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce 1.24 - moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto 1.25 + then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2) 1.26 + then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce 1.27 + moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto 1.28 ultimately show ?thesis by auto 1.29 next 1.30 assume "\<not>(\<exists>z. x < z \<and> z < y)" 1.31 then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto 1.32 define U where "U = {x<..}" 1.33 then have "open U" by simp 1.34 - moreover have "y \<in> U" using `x < y` U_def by simp 1.35 - ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto 1.36 - have "U = {y..}" unfolding U_def using * `x < y` by auto 1.37 - then have "V \<subseteq> {y..}" using `V \<subseteq> U` by simp 1.38 - then have "(LEAST w. w \<in> V) = y" using `y \<in> V` by (meson Least_equality atLeast_iff subsetCE) 1.39 - then have "y \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto 1.40 - moreover have "x < y \<and> y \<le> y" using `x < y` by simp 1.41 + moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp 1.42 + ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 1.43 + have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto 1.44 + then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp 1.45 + then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE) 1.46 + then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto 1.47 + moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp 1.48 ultimately show ?thesis by auto 1.49 qed 1.50 - moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp 1.51 + moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp 1.52 ultimately show ?thesis by auto 1.53 qed 1.54 1.55 @@ -538,9 +538,9 @@ 1.56 proof - 1.57 obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto 1.58 define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}" 1.59 - then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image) 1.60 + then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 1.61 define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}" 1.62 - then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image) 1.63 + then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image) 1.64 have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y 1.65 proof (cases) 1.66 assume "\<exists>z. x < z \<and> z < y" 1.67 @@ -548,27 +548,27 @@ 1.68 define U where "U = {x<..<y}" 1.69 then have "open U" by simp 1.70 moreover have "z \<in> U" using z U_def by simp 1.71 - ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto 1.72 + ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 1.73 define w where "w = (SOME x. x \<in> V)" 1.74 - then have "w \<in> V" using `z \<in> V` by (metis someI2) 1.75 - then have "x \<le> w \<and> w < y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce 1.76 - moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto 1.77 + then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2) 1.78 + then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce 1.79 + moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto 1.80 ultimately show ?thesis by auto 1.81 next 1.82 assume "\<not>(\<exists>z. x < z \<and> z < y)" 1.83 then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast 1.84 define U where "U = {..<y}" 1.85 then have "open U" by simp 1.86 - moreover have "x \<in> U" using `x < y` U_def by simp 1.87 - ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto 1.88 - have "U = {..x}" unfolding U_def using * `x < y` by auto 1.89 - then have "V \<subseteq> {..x}" using `V \<subseteq> U` by simp 1.90 - then have "(GREATEST x. x \<in> V) = x" using `x \<in> V` by (meson Greatest_equality atMost_iff subsetCE) 1.91 - then have "x \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto 1.92 - moreover have "x \<le> x \<and> x < y" using `x < y` by simp 1.93 + moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp 1.94 + ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto 1.95 + have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto 1.96 + then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp 1.97 + then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE) 1.98 + then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto 1.99 + moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp 1.100 ultimately show ?thesis by auto 1.101 qed 1.102 - moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp 1.103 + moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp 1.104 ultimately show ?thesis by auto 1.105 qed 1.106 1.107 @@ -579,10 +579,10 @@ 1.108 using countable_separating_set_linorder1 by auto 1.109 have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y 1.110 proof - 1.111 - obtain z where "x < z" "z < y" using `x < y` dense by blast 1.112 + obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast 1.113 then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto 1.114 - then have "x < b \<and> b < y" using `z < y` by auto 1.115 - then show ?thesis using `b \<in> B` by auto 1.116 + then have "x < b \<and> b < y" using \<open>z < y\<close> by auto 1.117 + then show ?thesis using \<open>b \<in> B\<close> by auto 1.118 qed 1.119 then show ?thesis using B(1) by auto 1.120 qed 1.121 @@ -680,7 +680,7 @@ 1.122 shows "openin T (\<Inter>i \<in> I. U i)" 1.123 proof - 1.124 have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T" 1.125 - using `I \<noteq> {}` openin_subset[OF assms(3)] by auto 1.126 + using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto 1.127 then show ?thesis 1.128 using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute) 1.129 qed