src/HOL/Analysis/Elementary_Normed_Spaces.thy
 changeset 70724 65371451fde8 parent 70690 8518a750f7bb child 70817 dd675800469d
equal 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>`
`    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 `