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