src/HOL/Analysis/Brouwer_Fixpoint.thy
 changeset 69508 2a4c8a2a3f8e parent 69325 4b6ddc5989fc child 69529 4ab9657b3257
1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Dec 26 20:57:23 2018 +0100
1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Dec 27 19:48:28 2018 +0100
1.3 @@ -1060,7 +1060,7 @@
1.5  text \<open>More properties of ARs, ANRs and ENRs\<close>
1.7 -lemma not_AR_empty [simp]: "~ AR({})"
1.8 +lemma not_AR_empty [simp]: "\<not> AR({})"
1.9    by (auto simp: AR_def)
1.11  lemma ENR_empty [simp]: "ENR {}"
1.12 @@ -3823,7 +3823,7 @@
1.13  lemma non_extensible_Borsuk_map:
1.14    fixes a :: "'a :: euclidean_space"
1.15    assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
1.16 -    shows "~ (\<exists>g. continuous_on (s \<union> c) g \<and>
1.17 +    shows "\<not> (\<exists>g. continuous_on (s \<union> c) g \<and>
1.18                    g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
1.19                    (\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
1.20  proof -
1.21 @@ -4534,7 +4534,7 @@
1.22    fixes a :: "'a :: euclidean_space"
1.23    assumes "compact S" and "a \<notin> S"
1.24     shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
1.25 -          ~(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
1.26 +          \<not>(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
1.27                                 (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
1.28     (is "?lhs = ?rhs")
1.29  proof (cases "S = {}")
1.30 @@ -4550,9 +4550,9 @@
1.31      by (simp add: \<open>a \<notin> S\<close>)
1.32    obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
1.33      using bounded_subset_ballD \<open>bounded S\<close> by blast
1.34 -  have "~ ?rhs \<longleftrightarrow> ~ ?lhs"
1.35 +  have "\<not> ?rhs \<longleftrightarrow> \<not> ?lhs"
1.36    proof
1.37 -    assume notr: "~ ?rhs"
1.38 +    assume notr: "\<not> ?rhs"
1.39      have nog: "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
1.40                     g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
1.41                     (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
1.42 @@ -4564,12 +4564,12 @@
1.43        using notr
1.44        by (auto simp: nullhomotopic_into_sphere_extension
1.45                   [OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
1.46 -    with \<open>a \<notin> S\<close> show  "~ ?lhs"
1.47 +    with \<open>a \<notin> S\<close> show  "\<not> ?lhs"
1.48        apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
1.49        apply (drule_tac x=g in spec)
1.50        using continuous_on_subset by fastforce
1.51    next
1.52 -    assume "~ ?lhs"
1.53 +    assume "\<not> ?lhs"
1.54      then obtain b where b: "b \<in> connected_component_set (- S) a" and "r \<le> norm b"
1.55        using bounded_iff linear by blast
1.56      then have bnot: "b \<notin> ball 0 r"
1.57 @@ -4593,7 +4593,7 @@
1.58      ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
1.59                           (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
1.60        by (meson homotopic_with_subset_left homotopic_with_trans r)
1.61 -    then show "~ ?rhs"
1.62 +    then show "\<not> ?rhs"
1.63        by blast
1.64    qed
1.65    then show ?thesis by blast