--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 13:59:10 2017 +0100
@@ -499,9 +499,9 @@
proof -
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}"
- then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
- then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y
proof (cases)
assume "\<exists>z. x < z \<and> z < y"
@@ -509,27 +509,27 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
+ ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
- then have "w \<in> V" using `z \<in> V` by (metis someI2)
- then have "x < w \<and> w \<le> y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce
- moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto
+ then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
+ then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
+ moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. x < z \<and> z < y)"
then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto
define U where "U = {x<..}"
then have "open U" by simp
- moreover have "y \<in> U" using `x < y` U_def by simp
- ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
- have "U = {y..}" unfolding U_def using * `x < y` by auto
- then have "V \<subseteq> {y..}" using `V \<subseteq> U` by simp
- then have "(LEAST w. w \<in> V) = y" using `y \<in> V` by (meson Least_equality atLeast_iff subsetCE)
- then have "y \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto
- moreover have "x < y \<and> y \<le> y" using `x < y` by simp
+ moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
+ ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
+ then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
+ then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
+ then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
+ moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp
ultimately show ?thesis by auto
qed
- moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp
+ moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
ultimately show ?thesis by auto
qed
@@ -538,9 +538,9 @@
proof -
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}"
- then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
- then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y
proof (cases)
assume "\<exists>z. x < z \<and> z < y"
@@ -548,27 +548,27 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
+ ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
- then have "w \<in> V" using `z \<in> V` by (metis someI2)
- then have "x \<le> w \<and> w < y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce
- moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto
+ then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
+ then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
+ moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. x < z \<and> z < y)"
then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast
define U where "U = {..<y}"
then have "open U" by simp
- moreover have "x \<in> U" using `x < y` U_def by simp
- ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
- have "U = {..x}" unfolding U_def using * `x < y` by auto
- then have "V \<subseteq> {..x}" using `V \<subseteq> U` by simp
- then have "(GREATEST x. x \<in> V) = x" using `x \<in> V` by (meson Greatest_equality atMost_iff subsetCE)
- then have "x \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto
- moreover have "x \<le> x \<and> x < y" using `x < y` by simp
+ moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
+ ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
+ then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
+ then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
+ then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
+ moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp
ultimately show ?thesis by auto
qed
- moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp
+ moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
ultimately show ?thesis by auto
qed
@@ -579,10 +579,10 @@
using countable_separating_set_linorder1 by auto
have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y
proof -
- obtain z where "x < z" "z < y" using `x < y` dense by blast
+ obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast
then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto
- then have "x < b \<and> b < y" using `z < y` by auto
- then show ?thesis using `b \<in> B` by auto
+ then have "x < b \<and> b < y" using \<open>z < y\<close> by auto
+ then show ?thesis using \<open>b \<in> B\<close> by auto
qed
then show ?thesis using B(1) by auto
qed
@@ -680,7 +680,7 @@
shows "openin T (\<Inter>i \<in> I. U i)"
proof -
have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
- using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
+ using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
then show ?thesis
using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed