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.4  
     1.5  text \<open>More properties of ARs, ANRs and ENRs\<close>
     1.6  
     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.10  
    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