2338 using injective_imp_isometric[OF assms(4,1,2,3)] by auto |
2338 using injective_imp_isometric[OF assms(4,1,2,3)] by auto |
2339 show ?thesis |
2339 show ?thesis |
2340 using complete_isometric_image[OF \<open>e>0\<close> assms(1,2) e] and assms(4) |
2340 using complete_isometric_image[OF \<open>e>0\<close> assms(1,2) e] and assms(4) |
2341 unfolding complete_eq_closed[symmetric] by auto |
2341 unfolding complete_eq_closed[symmetric] by auto |
2342 qed |
2342 qed |
|
2343 |
|
2344 |
|
2345 lemma closure_bounded_linear_image_subset: |
|
2346 assumes f: "bounded_linear f" |
|
2347 shows "f ` closure S \<subseteq> closure (f ` S)" |
|
2348 using linear_continuous_on [OF f] closed_closure closure_subset |
|
2349 by (rule image_closure_subset) |
|
2350 |
|
2351 lemma closure_linear_image_subset: |
|
2352 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector" |
|
2353 assumes "linear f" |
|
2354 shows "f ` (closure S) \<subseteq> closure (f ` S)" |
|
2355 using assms unfolding linear_conv_bounded_linear |
|
2356 by (rule closure_bounded_linear_image_subset) |
|
2357 |
|
2358 lemma closed_injective_linear_image: |
|
2359 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2360 assumes S: "closed S" and f: "linear f" "inj f" |
|
2361 shows "closed (f ` S)" |
|
2362 proof - |
|
2363 obtain g where g: "linear g" "g \<circ> f = id" |
|
2364 using linear_injective_left_inverse [OF f] by blast |
|
2365 then have confg: "continuous_on (range f) g" |
|
2366 using linear_continuous_on linear_conv_bounded_linear by blast |
|
2367 have [simp]: "g ` f ` S = S" |
|
2368 using g by (simp add: image_comp) |
|
2369 have cgf: "closed (g ` f ` S)" |
|
2370 by (simp add: \<open>g \<circ> f = id\<close> S image_comp) |
|
2371 have [simp]: "(range f \<inter> g -` S) = f ` S" |
|
2372 using g unfolding o_def id_def image_def by auto metis+ |
|
2373 show ?thesis |
|
2374 proof (rule closedin_closed_trans [of "range f"]) |
|
2375 show "closedin (top_of_set (range f)) (f ` S)" |
|
2376 using continuous_closedin_preimage [OF confg cgf] by simp |
|
2377 show "closed (range f)" |
|
2378 apply (rule closed_injective_image_subspace) |
|
2379 using f apply (auto simp: linear_linear linear_injective_0) |
|
2380 done |
|
2381 qed |
|
2382 qed |
|
2383 |
|
2384 lemma closed_injective_linear_image_eq: |
|
2385 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2386 assumes f: "linear f" "inj f" |
|
2387 shows "(closed(image f s) \<longleftrightarrow> closed s)" |
|
2388 by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff) |
|
2389 |
|
2390 lemma closure_injective_linear_image: |
|
2391 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2392 shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)" |
|
2393 apply (rule subset_antisym) |
|
2394 apply (simp add: closure_linear_image_subset) |
|
2395 by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono) |
|
2396 |
|
2397 lemma closure_bounded_linear_image: |
|
2398 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2399 shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)" |
|
2400 apply (rule subset_antisym, simp add: closure_linear_image_subset) |
|
2401 apply (rule closure_minimal, simp add: closure_subset image_mono) |
|
2402 by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) |
|
2403 |
|
2404 lemma closure_scaleR: |
|
2405 fixes S :: "'a::real_normed_vector set" |
|
2406 shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)" |
|
2407 proof |
|
2408 show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)" |
|
2409 using bounded_linear_scaleR_right |
|
2410 by (rule closure_bounded_linear_image_subset) |
|
2411 show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)" |
|
2412 by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) |
|
2413 qed |
2343 |
2414 |
2344 |
2415 |
2345 subsection\<^marker>\<open>tag unimportant\<close> \<open>Some properties of a canonical subspace\<close> |
2416 subsection\<^marker>\<open>tag unimportant\<close> \<open>Some properties of a canonical subspace\<close> |
2346 |
2417 |
2347 lemma closed_substandard: "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0}" |
2418 lemma closed_substandard: "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0}" |