src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 66793 deabce3ccf1f
parent 66643 f7e38b8583a0
child 66794 83bf64da6938
     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -676,6 +676,10 @@
     1.4      using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
     1.5  qed
     1.6  
     1.7 +lemma openin_Inter [intro]:
     1.8 +  assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
     1.9 +  by (metis (full_types) assms openin_INT2 image_ident)
    1.10 +
    1.11  
    1.12  subsubsection \<open>Closed sets\<close>
    1.13  
    1.14 @@ -2404,6 +2408,11 @@
    1.15  lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
    1.16    by (meson closedin_limpt closed_subset closedin_closed_trans)
    1.17  
    1.18 +lemma connected_closed_set:
    1.19 +   "closed S
    1.20 +    \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
    1.21 +  unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
    1.22 +
    1.23  lemma closedin_subset_trans:
    1.24    "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
    1.25      closedin (subtopology euclidean T) S"
    1.26 @@ -5407,6 +5416,13 @@
    1.27      by auto
    1.28  qed
    1.29  
    1.30 +lemma compact_Inter:
    1.31 +  fixes \<F> :: "'a :: heine_borel set set"
    1.32 +  assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
    1.33 +  shows "compact(\<Inter> \<F>)"
    1.34 +  using assms
    1.35 +  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
    1.36 +
    1.37  lemma compact_closure [simp]:
    1.38    fixes S :: "'a::heine_borel set"
    1.39    shows "compact(closure S) \<longleftrightarrow> bounded S"
    1.40 @@ -5819,19 +5835,6 @@
    1.41    then show ?thesis unfolding complete_def by auto
    1.42  qed
    1.43  
    1.44 -lemma nat_approx_posE:
    1.45 -  fixes e::real
    1.46 -  assumes "0 < e"
    1.47 -  obtains n :: nat where "1 / (Suc n) < e"
    1.48 -proof atomize_elim
    1.49 -  have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
    1.50 -    by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
    1.51 -  also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
    1.52 -    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
    1.53 -  also have "\<dots> = e" by simp
    1.54 -  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
    1.55 -qed
    1.56 -
    1.57  lemma compact_eq_totally_bounded:
    1.58    "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
    1.59      (is "_ \<longleftrightarrow> ?rhs")
    1.60 @@ -9679,6 +9682,43 @@
    1.61        simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
    1.62      done
    1.63  
    1.64 +lemma homeomorphic_ball01_UNIV:
    1.65 +  "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
    1.66 +  (is "?B homeomorphic ?U")
    1.67 +proof
    1.68 +  have "x \<in> (\<lambda>z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a
    1.69 +    apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI)
    1.70 +     apply (auto simp: divide_simps)
    1.71 +    using norm_ge_zero [of x] apply linarith+
    1.72 +    done
    1.73 +  then show "(\<lambda>z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U"
    1.74 +    by blast
    1.75 +  have "x \<in> range (\<lambda>z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a
    1.76 +    apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI)
    1.77 +    using that apply (auto simp: divide_simps)
    1.78 +    done
    1.79 +  then show "(\<lambda>z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B"
    1.80 +    by (force simp: divide_simps dest: add_less_zeroD)
    1.81 +  show "continuous_on (ball 0 1) (\<lambda>z. z /\<^sub>R (1 - norm z))"
    1.82 +    by (rule continuous_intros | force)+
    1.83 +  show "continuous_on UNIV (\<lambda>z. z /\<^sub>R (1 + norm z))"
    1.84 +    apply (intro continuous_intros)
    1.85 +    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
    1.86 +    done
    1.87 +  show "\<And>x. x \<in> ball 0 1 \<Longrightarrow>
    1.88 +         x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x"
    1.89 +    by (auto simp: divide_simps)
    1.90 +  show "\<And>y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y"
    1.91 +    apply (auto simp: divide_simps)
    1.92 +    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
    1.93 +    done
    1.94 +qed
    1.95 +
    1.96 +proposition homeomorphic_ball_UNIV:
    1.97 +  fixes a ::"'a::real_normed_vector"
    1.98 +  assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
    1.99 +  using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
   1.100 +
   1.101  subsection\<open>Inverse function property for open/closed maps\<close>
   1.102  
   1.103  lemma continuous_on_inverse_open_map:
   1.104 @@ -10711,7 +10751,7 @@
   1.105    then show ?thesis by blast
   1.106  qed
   1.107  
   1.108 -lemma closed_imp_fip_compact:
   1.109 +lemma clconnected_closedin_eqosed_imp_fip_compact:
   1.110    fixes S :: "'a::heine_borel set"
   1.111    shows
   1.112     "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
   1.113 @@ -11043,38 +11083,38 @@
   1.114  text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
   1.115  
   1.116  lemma continuous_disconnected_range_constant:
   1.117 -  assumes s: "connected s"
   1.118 -      and conf: "continuous_on s f"
   1.119 -      and fim: "f ` s \<subseteq> t"
   1.120 +  assumes S: "connected S"
   1.121 +      and conf: "continuous_on S f"
   1.122 +      and fim: "f ` S \<subseteq> t"
   1.123        and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
   1.124 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   1.125 -proof (cases "s = {}")
   1.126 +    shows "\<exists>a. \<forall>x \<in> S. f x = a"
   1.127 +proof (cases "S = {}")
   1.128    case True then show ?thesis by force
   1.129  next
   1.130    case False
   1.131 -  { fix x assume "x \<in> s"
   1.132 -    then have "f ` s \<subseteq> {f x}"
   1.133 -    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
   1.134 +  { fix x assume "x \<in> S"
   1.135 +    then have "f ` S \<subseteq> {f x}"
   1.136 +    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   1.137    }
   1.138    with False show ?thesis
   1.139      by blast
   1.140  qed
   1.141  
   1.142  lemma discrete_subset_disconnected:
   1.143 -  fixes s :: "'a::topological_space set"
   1.144 +  fixes S :: "'a::topological_space set"
   1.145    fixes t :: "'b::real_normed_vector set"
   1.146 -  assumes conf: "continuous_on s f"
   1.147 -      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   1.148 -   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
   1.149 -proof -
   1.150 -  { fix x assume x: "x \<in> s"
   1.151 -    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
   1.152 +  assumes conf: "continuous_on S f"
   1.153 +      and no: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   1.154 +   shows "f ` S \<subseteq> {y. connected_component_set (f ` S) y = {y}}"
   1.155 +proof -
   1.156 +  { fix x assume x: "x \<in> S"
   1.157 +    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> S; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
   1.158        using conf no [OF x] by auto
   1.159      then have e2: "0 \<le> e / 2"
   1.160        by simp
   1.161 -    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
   1.162 +    have "f y = f x" if "y \<in> S" and ccs: "f y \<in> connected_component_set (f ` S) (f x)" for y
   1.163        apply (rule ccontr)
   1.164 -      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
   1.165 +      using connected_closed [of "connected_component_set (f ` S) (f x)"] \<open>e>0\<close>
   1.166        apply (simp add: del: ex_simps)
   1.167        apply (drule spec [where x="cball (f x) (e / 2)"])
   1.168        apply (drule spec [where x="- ball(f x) e"])
   1.169 @@ -11082,11 +11122,11 @@
   1.170          apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
   1.171         using centre_in_cball connected_component_refl_eq e2 x apply blast
   1.172        using ccs
   1.173 -      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
   1.174 +      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> S\<close>])
   1.175        done
   1.176 -    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
   1.177 +    moreover have "connected_component_set (f ` S) (f x) \<subseteq> f ` S"
   1.178        by (auto simp: connected_component_in)
   1.179 -    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
   1.180 +    ultimately have "connected_component_set (f ` S) (f x) = {f x}"
   1.181        by (auto simp: x)
   1.182    }
   1.183    with assms show ?thesis
   1.184 @@ -11094,22 +11134,22 @@
   1.185  qed
   1.186  
   1.187  lemma finite_implies_discrete:
   1.188 -  fixes s :: "'a::topological_space set"
   1.189 -  assumes "finite (f ` s)"
   1.190 -  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
   1.191 -proof -
   1.192 -  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
   1.193 -  proof (cases "f ` s - {f x} = {}")
   1.194 +  fixes S :: "'a::topological_space set"
   1.195 +  assumes "finite (f ` S)"
   1.196 +  shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
   1.197 +proof -
   1.198 +  have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
   1.199 +  proof (cases "f ` S - {f x} = {}")
   1.200      case True
   1.201      with zero_less_numeral show ?thesis
   1.202        by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
   1.203    next
   1.204      case False
   1.205 -    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
   1.206 +    then obtain z where z: "z \<in> S" "f z \<noteq> f x"
   1.207        by blast
   1.208 -    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
   1.209 +    have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
   1.210        using assms by simp
   1.211 -    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
   1.212 +    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
   1.213        apply (rule finite_imp_less_Inf)
   1.214        using z apply force+
   1.215        done
   1.216 @@ -11123,20 +11163,20 @@
   1.217  text\<open>This proof requires the existence of two separate values of the range type.\<close>
   1.218  lemma finite_range_constant_imp_connected:
   1.219    assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   1.220 -              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
   1.221 -    shows "connected s"
   1.222 +              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
   1.223 +    shows "connected S"
   1.224  proof -
   1.225    { fix t u
   1.226 -    assume clt: "closedin (subtopology euclidean s) t"
   1.227 -       and clu: "closedin (subtopology euclidean s) u"
   1.228 -       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
   1.229 -    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
   1.230 +    assume clt: "closedin (subtopology euclidean S) t"
   1.231 +       and clu: "closedin (subtopology euclidean S) u"
   1.232 +       and tue: "t \<inter> u = {}" and tus: "t \<union> u = S"
   1.233 +    have conif: "continuous_on S (\<lambda>x. if x \<in> t then 0 else 1)"
   1.234        apply (subst tus [symmetric])
   1.235        apply (rule continuous_on_cases_local)
   1.236        using clt clu tue
   1.237        apply (auto simp: tus continuous_on_const)
   1.238        done
   1.239 -    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
   1.240 +    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
   1.241        by (rule finite_subset [of _ "{0,1}"]) auto
   1.242      have "t = {} \<or> u = {}"
   1.243        using assms [OF conif fi] tus [symmetric]