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
```