src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 70724 65371451fde8
parent 70690 8518a750f7bb
child 70817 dd675800469d
equal deleted inserted replaced
70723:4e39d87c9737 70724:65371451fde8
     7 section \<open>Elementary Normed Vector Spaces\<close>
     7 section \<open>Elementary Normed Vector Spaces\<close>
     8 
     8 
     9 theory Elementary_Normed_Spaces
     9 theory Elementary_Normed_Spaces
    10   imports
    10   imports
    11   "HOL-Library.FuncSet"
    11   "HOL-Library.FuncSet"
    12   Elementary_Metric_Spaces Linear_Algebra
    12   Elementary_Metric_Spaces Cartesian_Space
    13   Connected
    13   Connected
    14 begin
    14 begin
       
    15 subsection \<open>Orthogonal Transformation of Balls\<close>
    15 
    16 
    16 subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
    17 subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
    17 
       
    18 lemma countable_PiE:
       
    19   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
       
    20   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
       
    21 
       
    22 
    18 
    23 lemma open_sums:
    19 lemma open_sums:
    24   fixes T :: "('b::real_normed_vector) set"
    20   fixes T :: "('b::real_normed_vector) set"
    25   assumes "open S \<or> open T"
    21   assumes "open S \<or> open T"
    26   shows "open (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
    22   shows "open (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
    49     then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y"
    45     then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y"
    50       by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm)
    46       by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm)
    51     then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)"
    47     then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)"
    52       using \<open>0 < e\<close> \<open>y \<in> T\<close> by blast
    48       using \<open>0 < e\<close> \<open>y \<in> T\<close> by blast
    53   qed
    49   qed
       
    50 qed
       
    51 
       
    52 lemma image_orthogonal_transformation_ball:
       
    53   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
       
    54   assumes "orthogonal_transformation f"
       
    55   shows "f ` ball x r = ball (f x) r"
       
    56 proof (intro equalityI subsetI)
       
    57   fix y assume "y \<in> f ` ball x r"
       
    58   with assms show "y \<in> ball (f x) r"
       
    59     by (auto simp: orthogonal_transformation_isometry)
       
    60 next
       
    61   fix y assume y: "y \<in> ball (f x) r"
       
    62   then obtain z where z: "y = f z"
       
    63     using assms orthogonal_transformation_surj by blast
       
    64   with y assms show "y \<in> f ` ball x r"
       
    65     by (auto simp: orthogonal_transformation_isometry)
       
    66 qed
       
    67 
       
    68 lemma image_orthogonal_transformation_cball:
       
    69   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
       
    70   assumes "orthogonal_transformation f"
       
    71   shows "f ` cball x r = cball (f x) r"
       
    72 proof (intro equalityI subsetI)
       
    73   fix y assume "y \<in> f ` cball x r"
       
    74   with assms show "y \<in> cball (f x) r"
       
    75     by (auto simp: orthogonal_transformation_isometry)
       
    76 next
       
    77   fix y assume y: "y \<in> cball (f x) r"
       
    78   then obtain z where z: "y = f z"
       
    79     using assms orthogonal_transformation_surj by blast
       
    80   with y assms show "y \<in> f ` cball x r"
       
    81     by (auto simp: orthogonal_transformation_isometry)
    54 qed
    82 qed
    55 
    83 
    56 
    84 
    57 subsection \<open>Support\<close>
    85 subsection \<open>Support\<close>
    58 
    86