Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Abstract_Euclidean_Space.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Author:  LCP, ported from HOL Light
*)

section\<open>Euclidean space and n-spheres, as subtopologies of n-dimensional space\<close>

theory Abstract_Euclidean_Space
imports Homotopy Locally
begin

subsection \<open>Euclidean spaces as abstract topologies\<close>

definition Euclidean_space :: "nat \ (nat \ real) topology"
  where "Euclidean_space n \ subtopology (powertop_real UNIV) {x. \i\n. x i = 0}"

lemma topspace_Euclidean_space:
   "topspace(Euclidean_space n) = {x. \i\n. x i = 0}"
  by (simp add: Euclidean_space_def)

lemma nonempty_Euclidean_space: "topspace(Euclidean_space n) \ {}"
  by (force simp: topspace_Euclidean_space)

lemma subset_Euclidean_space [simp]:
   "topspace(Euclidean_space m) \ topspace(Euclidean_space n) \ m \ n"
  apply (simp add: topspace_Euclidean_space subset_iff, safe)
   apply (drule_tac x="(\i. if i < m then 1 else 0)" in spec)
   apply auto
  using not_less by fastforce

lemma topspace_Euclidean_space_alt:
  "topspace(Euclidean_space n) = (\i \ {n..}. {x. x \ topspace(powertop_real UNIV) \ x i \ {0}})"
  by (auto simp: topspace_Euclidean_space)

lemma closedin_Euclidean_space:
  "closedin (powertop_real UNIV) (topspace(Euclidean_space n))"
proof -
  have "closedin (powertop_real UNIV) {x. x i = 0}" if "n \ i" for i
  proof -
    have "closedin (powertop_real UNIV) {x \ topspace (powertop_real UNIV). x i \ {0}}"
    proof (rule closedin_continuous_map_preimage)
      show "continuous_map (powertop_real UNIV) euclideanreal (\x. x i)"
        by (metis UNIV_I continuous_map_product_coordinates)
      show "closedin euclideanreal {0}"
        by simp
    qed
    then show ?thesis
      by auto
  qed
  then show ?thesis
    unfolding topspace_Euclidean_space_alt
    by force
qed

lemma closedin_Euclidean_imp_closed: "closedin (Euclidean_space m) S \ closed S"
  by (metis Euclidean_space_def closed_closedin closedin_Euclidean_space closedin_closed_subtopology euclidean_product_topology topspace_Euclidean_space)

lemma closedin_Euclidean_space_iff:
  "closedin (Euclidean_space m) S \ closed S \ S \ topspace (Euclidean_space m)"
  (is "?lhs \ ?rhs")
proof
  show "?lhs \ ?rhs"
    using closedin_closed_subtopology topspace_Euclidean_space
    by (fastforce simp: topspace_Euclidean_space_alt closedin_Euclidean_imp_closed)
  show "?rhs \ ?lhs"
  apply (simp add: closedin_subtopology Euclidean_space_def)
    by (metis (no_types) closed_closedin euclidean_product_topology inf.orderE)
qed

lemma continuous_map_componentwise_Euclidean_space:
  "continuous_map X (Euclidean_space n) (\x i. if i < n then f x i else 0) \
   (\<forall>i < n. continuous_map X euclideanreal (\<lambda>x. f x i))"
proof -
  have *: "continuous_map X euclideanreal (\x. if k < n then f x k else 0)"
    if "\i. i continuous_map X euclideanreal (\x. f x i)" for k
    by (intro continuous_intros that)
  show ?thesis
    unfolding Euclidean_space_def continuous_map_in_subtopology
    by (fastforce simp: continuous_map_componentwise_UNIV * elim: continuous_map_eq)
qed

lemma continuous_map_Euclidean_space_add [continuous_intros]:
   "\continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\
    \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
  unfolding Euclidean_space_def continuous_map_in_subtopology
  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_add)

lemma continuous_map_Euclidean_space_diff [continuous_intros]:
   "\continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\
    \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
  unfolding Euclidean_space_def continuous_map_in_subtopology
  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)

lemma continuous_map_Euclidean_space_iff:
  "continuous_map (Euclidean_space m) euclidean g
   = continuous_on (topspace (Euclidean_space m)) g"
proof
  assume "continuous_map (Euclidean_space m) euclidean g"
  then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclidean g"
    by (simp add: Euclidean_space_def euclidean_product_topology)
  then show "continuous_on (topspace (Euclidean_space m)) g"
    by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space)
next
  assume "continuous_on (topspace (Euclidean_space m)) g"
  then have "continuous_map (top_of_set {f. \n\m. f n = 0}) euclidean g"
    by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space)
  then show "continuous_map (Euclidean_space m) euclidean g"
    by (simp add: Euclidean_space_def euclidean_product_topology)
qed

lemma cm_Euclidean_space_iff_continuous_on:
  "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f
   \<longleftrightarrow> continuous_on (topspace (subtopology (Euclidean_space m) S)) f \<and>
       f ` (topspace (subtopology (Euclidean_space m) S)) \<subseteq> topspace (Euclidean_space n)"
  (is "?P \ ?Q \ ?R")
proof -
  have ?Q if ?P
  proof -
    have "\n. Euclidean_space n = top_of_set {f. \m\n. f m = 0}"
      by (simp add: Euclidean_space_def euclidean_product_topology)
    with that show ?thesis
      by (simp add: subtopology_subtopology)
  qed
  moreover
  have ?R if ?P
    using that by (simp add: image_subset_iff continuous_map_def)
  moreover
  have ?P if ?Q ?R
  proof -
    have "continuous_map (top_of_set (topspace (subtopology (subtopology (powertop_real UNIV) {f. \n\m. f n = 0}) S))) (top_of_set (topspace (subtopology (powertop_real UNIV) {f. \na\n. f na = 0}))) f"
      using Euclidean_space_def that by auto
    then show ?thesis
      by (simp add: Euclidean_space_def euclidean_product_topology subtopology_subtopology)
  qed
  ultimately show ?thesis
    by auto
qed

lemma homeomorphic_Euclidean_space_product_topology:
  "Euclidean_space n homeomorphic_space product_topology (\i. euclideanreal) {..
proof -
  have cm: "continuous_map (product_topology (\i. euclideanreal) {..
          euclideanreal (\<lambda>x. if k < n then x k else 0)" for k
    by (auto intro: continuous_map_if continuous_map_product_projection)
  show ?thesis
    unfolding homeomorphic_space_def homeomorphic_maps_def
    apply (rule_tac x="\f. restrict f {..
    apply (rule_tac x="\f i. if i < n then f i else 0" in exI)
    apply (simp add: Euclidean_space_def continuous_map_in_subtopology)
    apply (intro conjI continuous_map_from_subtopology)
       apply (force simp: continuous_map_componentwise cm intro: continuous_map_product_projection)+
    done
qed

lemma contractible_Euclidean_space [simp]: "contractible_space (Euclidean_space n)"
  using homeomorphic_Euclidean_space_product_topology contractible_space_euclideanreal
    contractible_space_product_topology homeomorphic_space_contractibility by blast

lemma path_connected_Euclidean_space: "path_connected_space (Euclidean_space n)"
  by (simp add: contractible_imp_path_connected_space)

lemma connected_Euclidean_space: "connected_space (Euclidean_space n)"
  by (simp add: contractible_imp_connected_space)

lemma locally_path_connected_Euclidean_space:
   "locally_path_connected_space (Euclidean_space n)"
  apply (simp add: homeomorphic_locally_path_connected_space [OF homeomorphic_Euclidean_space_product_topology [of n]]
                   locally_path_connected_space_product_topology)
  using locally_path_connected_space_euclideanreal by auto

lemma compact_Euclidean_space:
   "compact_space (Euclidean_space n) \ n = 0"
  by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology)

subsection\<open>n-dimensional spheres\<close>

definition nsphere where
"nsphere n \ subtopology (Euclidean_space (Suc n)) { x. (\i\n. x i ^ 2) = 1 }"

lemma nsphere:
   "nsphere n = subtopology (powertop_real UNIV)
                            {x. (\<Sum>i\<le>n. x i ^ 2) = 1 \<and> (\<forall>i>n. x i = 0)}"
  by (simp add: nsphere_def Euclidean_space_def subtopology_subtopology Suc_le_eq Collect_conj_eq Int_commute)

lemma continuous_map_nsphere_projection: "continuous_map (nsphere n) euclideanreal (\x. x k)"
  unfolding nsphere
  by (blast intro: continuous_map_from_subtopology [OF continuous_map_product_projection])

lemma in_topspace_nsphere: "(\n. if n = 0 then 1 else 0) \ topspace (nsphere n)"
  by (simp add: nsphere_def topspace_Euclidean_space power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong)

lemma nonempty_nsphere [simp]: "~ (topspace(nsphere n) = {})"
  using in_topspace_nsphere by auto

lemma subtopology_nsphere_equator:
  "subtopology (nsphere (Suc n)) {x. x(Suc n) = 0} = nsphere n"
proof -
  have "({x. (\i\n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \ (\i>Suc n. x i = 0)} \ {x. x (Suc n) = 0})
      = {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>i>n. x i = (0::real))}"
    using Suc_lessI [of n] by (fastforce simp: set_eq_iff)
  then show ?thesis
    by (simp add: nsphere subtopology_subtopology)
qed

lemma topspace_nsphere_minus1:
  assumes x: "x \ topspace (nsphere n)" and "x n = 0"
  shows "x \ topspace (nsphere (n - Suc 0))"
proof (cases "n = 0")
  case True
  then show ?thesis
    using x by auto
next
  case False
  have subt_eq: "nsphere (n - Suc 0) = subtopology (nsphere n) {x. x n = 0}"
    by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
  with x show ?thesis
    by (simp add: assms)
qed

lemma continuous_map_nsphere_reflection:
  "continuous_map (nsphere n) (nsphere n) (\x i. if i = k then -x i else x i)"
proof -
  have cm: "continuous_map (powertop_real UNIV) euclideanreal (\x. if j = k then - x j else x j)" for j
  proof (cases "j=k")
    case True
    then show ?thesis
      by simp (metis UNIV_I continuous_map_product_projection)
  next
    case False
    then show ?thesis
      by (auto intro: continuous_map_product_projection)
  qed
  have eq: "(if i = k then x k * x k else x i * x i) = x i * x i" for i and x :: "nat \ real"
    by simp
  show ?thesis
    apply (simp add: nsphere continuous_map_in_subtopology continuous_map_componentwise_UNIV
                     continuous_map_from_subtopology cm)
    apply (intro conjI allI impI continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
      apply (auto simp: power2_eq_square if_distrib [where f = "\x. x * _"] eq cong: if_cong)
    done
qed

proposition contractible_space_upper_hemisphere:
  assumes "k \ n"
  shows "contractible_space(subtopology (nsphere n) {x. x k \ 0})"
proof -
  define p:: "nat \ real" where "p \ \i. if i = k then 1 else 0"
  have "p \ topspace(nsphere n)"
    using assms
    by (simp add: nsphere p_def power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong)
  let ?g = "\x i. x i / sqrt(\j\n. x j ^ 2)"
  let ?h = "\(t,q) i. (1 - t) * q i + t * p i"
  let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \ x k \ (\i\n. x i \ 0)}"
  have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \ x k}))
                       (subtopology (nsphere n) {x. 0 \<le> x k}) (?g \<circ> ?h)"
  proof (rule continuous_map_compose)
    have *: "\0 \ b k; (\i\n. (b i)\<^sup>2) = 1; \i>n. b i = 0; 0 \ a; a \ 1\
           \<Longrightarrow> \<exists>i. (i = k \<longrightarrow> (1 - a) * b k + a \<noteq> 0) \<and>
                   (i \<noteq> k \<longrightarrow> i \<le> n \<and> a \<noteq> 1 \<and> b i \<noteq> 0)" for a::real and b
      apply (cases "a \ 1 \ b k = 0"; simp)
       apply (metis (no_types, lifting) atMost_iff sum.neutral zero_power2)
      by (metis add.commute add_le_same_cancel2 diff_ge_0_iff_ge diff_zero less_eq_real_def mult_eq_0_iff mult_nonneg_nonneg not_le numeral_One zero_neq_numeral)
    show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \ x k})) ?Y ?h"
      using assms
      apply (auto simp: * nsphere continuous_map_componentwise_UNIV
               prod_topology_subtopology subtopology_subtopology case_prod_unfold
               continuous_map_in_subtopology Euclidean_space_def p_def if_distrib [where f = "\x. _ * x"] cong: if_cong)
      apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology)
        apply auto
      done
  next
    have 1: "\x i. \ i \ n; x i \ 0\ \ (\i\n. (x i / sqrt (\j\n. (x j)\<^sup>2))\<^sup>2) = 1"
      by (force simp: sum_nonneg sum_nonneg_eq_0_iff field_split_simps simp flip: sum_divide_distrib)
    have cm: "continuous_map ?Y (nsphere n) (\x i. x i / sqrt (\j\n. (x j)\<^sup>2))"
      unfolding Euclidean_space_def nsphere subtopology_subtopology continuous_map_in_subtopology
    proof (intro continuous_intros conjI)
      show "continuous_map
               (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}))
               (powertop_real UNIV) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
        unfolding continuous_map_componentwise
        by (intro continuous_intros conjI ballI) (auto simp: sum_nonneg_eq_0_iff)
    qed (auto simp: 1)
    show "continuous_map ?Y (subtopology (nsphere n) {x. 0 \ x k}) (\x i. x i / sqrt (\j\n. (x j)\<^sup>2))"
      by (force simp: cm sum_nonneg continuous_map_in_subtopology if_distrib [where f = "\x. _ * x"] cong: if_cong)
  qed
  moreover have "(?g \ ?h) (0, x) = x"
    if "x \ topspace (subtopology (nsphere n) {x. 0 \ x k})" for x
    using that
    by (simp add: assms nsphere)
  moreover
  have "(?g \ ?h) (1, x) = p"
    if "x \ topspace (subtopology (nsphere n) {x. 0 \ x k})" for x
    by (force simp: assms p_def power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong)
  ultimately
  show ?thesis
    apply (simp add: contractible_space_def homotopic_with)
    apply (rule_tac x=p in exI)
    apply (rule_tac x="?g \ ?h" in exI, force)
    done
qed

corollary contractible_space_lower_hemisphere:
  assumes "k \ n"
  shows "contractible_space(subtopology (nsphere n) {x. x k \ 0})"
proof -
  have "contractible_space (subtopology (nsphere n) {x. 0 \ x k}) = ?thesis"
  proof (rule homeomorphic_space_contractibility)
    show "subtopology (nsphere n) {x. 0 \ x k} homeomorphic_space subtopology (nsphere n) {x. x k \ 0}"
      unfolding homeomorphic_space_def homeomorphic_maps_def
      apply (rule_tac x="\x i. if i = k then -(x i) else x i" in exI)+
      apply (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology
                  continuous_map_nsphere_reflection)
      done
  qed
  then show ?thesis
    using contractible_space_upper_hemisphere [OF assms] by metis
qed

proposition nullhomotopic_nonsurjective_sphere_map:
  assumes f: "continuous_map (nsphere p) (nsphere p) f"
    and fim: "f ` (topspace(nsphere p)) \ topspace(nsphere p)"
  obtains a where "homotopic_with (\x. True) (nsphere p) (nsphere p) f (\x. a)"
proof -
  obtain a where a: "a \ topspace(nsphere p)" "a \ f ` (topspace(nsphere p))"
    using fim continuous_map_image_subset_topspace f by blast
  then have a1: "(\i\p. (a i)\<^sup>2) = 1" and a0: "\i. i > p \ a i = 0"
    by (simp_all add: nsphere)
  have f1: "(\j\p. (f x j)\<^sup>2) = 1" if "x \ topspace (nsphere p)" for x
  proof -
    have "f x \ topspace (nsphere p)"
      using continuous_map_image_subset_topspace f that by blast
    then show ?thesis
      by (simp add: nsphere)
  qed
  show thesis
  proof
    let ?g = "\x i. x i / sqrt(\j\p. x j ^ 2)"
    let ?h = "\(t,x) i. (1 - t) * f x i - t * a i"
    let ?Y = "subtopology (Euclidean_space(Suc p)) (- {\i. 0})"
    let ?T01 = "top_of_set {0..1::real}"
    have 1: "continuous_map (prod_topology ?T01 (nsphere p)) (nsphere p) (?g \ ?h)"
    proof (rule continuous_map_compose)
      have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal ((\x. f x k) \ snd)" for k
        unfolding nsphere
        apply (simp add: continuous_map_of_snd)
        apply (rule continuous_map_compose [of _ "nsphere p" f, unfolded o_def])
        using f apply (simp add: nsphere)
        by (simp add: continuous_map_nsphere_projection)
      then have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal (\r. ?h r k)"
        for k
        unfolding case_prod_unfold o_def
        by (intro continuous_map_into_fulltopology [OF continuous_map_fst] continuous_intros) auto
      moreover have "?h ` ({0..1} \ topspace (nsphere p)) \ {x. \i\Suc p. x i = 0}"
        using continuous_map_image_subset_topspace [OF f]
        by (auto simp: nsphere image_subset_iff a0)
      moreover have "(\i. 0) \ ?h ` ({0..1} \ topspace (nsphere p))"
      proof clarify
        fix t b
        assume eq: "(\i. 0) = (\i. (1 - t) * f b i - t * a i)" and "t \ {0..1}" and b: "b \ topspace (nsphere p)"
        have "(1 - t)\<^sup>2 = (\i\p. ((1 - t) * f b i)^2)"
          using f1 [OF b] by (simp add: power_mult_distrib flip: sum_distrib_left)
        also have "\ = (\i\p. (t * a i)^2)"
          using eq by (simp add: fun_eq_iff)
        also have "\ = t\<^sup>2"
          using a1 by (simp add: power_mult_distrib flip: sum_distrib_left)
        finally have "1 - t = t"
          by (simp add: power2_eq_iff)
        then have *: "t = 1/2"
          by simp
        have fba: "f b \ a"
          using a(2) b by blast
        then show False
          using eq unfolding * by (simp add: fun_eq_iff)
      qed
      ultimately show "continuous_map (prod_topology ?T01 (nsphere p)) ?Y ?h"
        by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV)
    next
      have *: "\\i\Suc p. x i = 0; x \ (\i. 0)\ \ (\j\p. (x j)\<^sup>2) \ 0" for x :: "nat \ real"
        by (force simp: fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff)
      show "continuous_map ?Y (nsphere p) ?g"
        apply (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
                         nsphere continuous_map_componentwise subtopology_subtopology)
        apply (intro conjI allI continuous_intros continuous_map_from_subtopology [OF continuous_map_product_projection])
            apply (simp_all add: *)
         apply (force simp: sum_nonneg fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff power_divide simp flip: sum_divide_distrib)
        done
    qed
    have 2: "(?g \ ?h) (0, x) = f x" if "x \ topspace (nsphere p)" for x
      using that f1 by simp
    have 3: "(?g \ ?h) (1, x) = (\i. - a i)" for x
      using a by (force simp: field_split_simps nsphere)
    then show "homotopic_with (\x. True) (nsphere p) (nsphere p) f (\x. (\i. - a i))"
      by (force simp: homotopic_with intro: 1 2 3)
  qed
qed

lemma Hausdorff_Euclidean_space:
   "Hausdorff_space (Euclidean_space n)"
  unfolding Euclidean_space_def
  by (rule Hausdorff_space_subtopology) (metis Hausdorff_space_euclidean Hausdorff_space_product_topology)

end

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.