src/HOL/Homology/Invariance_of_Domain.thy
 author paulson Thu Apr 11 15:26:04 2019 +0100 (6 months ago) changeset 70125 b601c2c87076 parent 70114 089c17514794 child 70136 f03a01a18c6e permissions -rw-r--r--
type instantiations for poly_mapping as a real_normed_vector
 lp15@70097 ` 1` ```section\Invariance of Domain\ ``` lp15@70097 ` 2` lp15@70097 ` 3` ```theory Invariance_of_Domain ``` lp15@70114 ` 4` ``` imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism" ``` lp15@70097 ` 5` lp15@70097 ` 6` ```begin ``` lp15@70097 ` 7` lp15@70097 ` 8` ```subsection\Degree invariance mod 2 for map between pairs\ ``` lp15@70097 ` 9` lp15@70097 ` 10` ```theorem Borsuk_odd_mapping_degree_step: ``` lp15@70097 ` 11` ``` assumes cmf: "continuous_map (nsphere n) (nsphere n) f" ``` lp15@70097 ` 12` ``` and f: "\x. x \ topspace(nsphere n) \ (f \ (\x i. -x i)) x = ((\x i. -x i) \ f) x" ``` lp15@70097 ` 13` ``` and fim: "f ` (topspace(nsphere(n - Suc 0))) \ topspace(nsphere(n - Suc 0))" ``` lp15@70097 ` 14` ``` shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)" ``` lp15@70097 ` 15` ```proof (cases "n = 0") ``` lp15@70097 ` 16` ``` case False ``` lp15@70097 ` 17` ``` define neg where "neg \ \x::nat\real. \i. -x i" ``` lp15@70097 ` 18` ``` define upper where "upper \ \n. {x::nat\real. x n \ 0}" ``` lp15@70097 ` 19` ``` define lower where "lower \ \n. {x::nat\real. x n \ 0}" ``` lp15@70097 ` 20` ``` define equator where "equator \ \n. {x::nat\real. x n = 0}" ``` lp15@70097 ` 21` ``` define usphere where "usphere \ \n. subtopology (nsphere n) (upper n)" ``` lp15@70097 ` 22` ``` define lsphere where "lsphere \ \n. subtopology (nsphere n) (lower n)" ``` lp15@70097 ` 23` ``` have [simp]: "neg x i = -x i" for x i ``` lp15@70097 ` 24` ``` by (force simp: neg_def) ``` lp15@70097 ` 25` ``` have equator_upper: "equator n \ upper n" ``` lp15@70097 ` 26` ``` by (force simp: equator_def upper_def) ``` lp15@70097 ` 27` ``` have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n" ``` lp15@70097 ` 28` ``` by (simp add: usphere_def) ``` lp15@70097 ` 29` ``` let ?rhgn = "relative_homology_group n (nsphere n)" ``` lp15@70097 ` 30` ``` let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)" ``` lp15@70097 ` 31` ``` interpret GE: comm_group "?rhgn (equator n)" ``` lp15@70097 ` 32` ``` by simp ``` lp15@70097 ` 33` ``` interpret HB: group_hom "?rhgn (equator n)" ``` lp15@70097 ` 34` ``` "homology_group (int n - 1) (subtopology (nsphere n) (equator n))" ``` lp15@70097 ` 35` ``` "hom_boundary n (nsphere n) (equator n)" ``` lp15@70097 ` 36` ``` by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom) ``` lp15@70097 ` 37` ``` interpret HIU: group_hom "?rhgn (equator n)" ``` lp15@70097 ` 38` ``` "?rhgn (upper n)" ``` lp15@70097 ` 39` ``` "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id" ``` lp15@70097 ` 40` ``` by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) ``` lp15@70097 ` 41` ``` have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)" ``` lp15@70097 ` 42` ``` by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator) ``` lp15@70097 ` 43` ``` then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)" ``` lp15@70097 ` 44` ``` "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)" ``` lp15@70097 ` 45` ``` "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)" ``` lp15@70097 ` 46` ``` using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong) ``` lp15@70097 ` 47` ``` have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f" ``` lp15@70097 ` 48` ``` by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology) ``` lp15@70097 ` 49` lp15@70097 ` 50` ``` have "f x n = 0" if "x \ topspace (nsphere n)" "x n = 0" for x ``` lp15@70097 ` 51` ``` proof - ``` lp15@70097 ` 52` ``` have "x \ topspace (nsphere (n - Suc 0))" ``` lp15@70097 ` 53` ``` by (simp add: that topspace_nsphere_minus1) ``` lp15@70097 ` 54` ``` moreover have "topspace (nsphere n) \ {f. f n = 0} = topspace (nsphere (n - Suc 0))" ``` lp15@70097 ` 55` ``` by (metis subt_eq topspace_subtopology) ``` lp15@70097 ` 56` ``` ultimately show ?thesis ``` lp15@70097 ` 57` ``` using cmr continuous_map_def by fastforce ``` lp15@70097 ` 58` ``` qed ``` lp15@70097 ` 59` ``` then have fimeq: "f ` (topspace (nsphere n) \ equator n) \ topspace (nsphere n) \ equator n" ``` lp15@70097 ` 60` ``` using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff) ``` lp15@70097 ` 61` ``` have "\k. continuous_map (powertop_real UNIV) euclideanreal (\x. - x k)" ``` lp15@70097 ` 62` ``` by (metis UNIV_I continuous_map_product_projection continuous_map_minus) ``` lp15@70097 ` 63` ``` then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m ``` lp15@70097 ` 64` ``` by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology) ``` lp15@70097 ` 65` ``` then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg" ``` lp15@70097 ` 66` ``` by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology) ``` lp15@70097 ` 67` ``` have neg_in_top_iff: "neg x \ topspace(nsphere m) \ x \ topspace(nsphere m)" for m x ``` lp15@70097 ` 68` ``` by (simp add: nsphere_def neg_def topspace_Euclidean_space) ``` lp15@70097 ` 69` ``` obtain z where zcarr: "z \ carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" ``` lp15@70097 ` 70` ``` and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} ``` lp15@70097 ` 71` ``` = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" ``` lp15@70097 ` 72` ``` using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def) ``` lp15@70097 ` 73` ``` have "hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0} ``` lp15@70097 ` 74` ``` \ Group.iso (relative_homology_group n ``` lp15@70097 ` 75` ``` (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 76` ``` (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" ``` lp15@70097 ` 77` ``` using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp ``` lp15@70097 ` 78` ``` then obtain gp where g: "group_isomorphisms ``` lp15@70097 ` 79` ``` (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 80` ``` (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) ``` lp15@70097 ` 81` ``` (hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 82` ``` gp" ``` lp15@70097 ` 83` ``` by (auto simp: group.iso_iff_group_isomorphisms) ``` lp15@70097 ` 84` ``` then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" ``` lp15@70097 ` 85` ``` "relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}" gp ``` lp15@70097 ` 86` ``` by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def) ``` lp15@70097 ` 87` ``` obtain zp where zpcarr: "zp \ carrier(relative_homology_group n (lsphere n) (equator n))" ``` lp15@70097 ` 88` ``` and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z" ``` lp15@70097 ` 89` ``` and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp} ``` lp15@70097 ` 90` ``` = relative_homology_group n (lsphere n) (equator n)" ``` lp15@70097 ` 91` ``` proof ``` lp15@70097 ` 92` ``` show "gp z \ carrier (relative_homology_group n (lsphere n) (equator n))" ``` lp15@70097 ` 93` ``` "hom_boundary n (lsphere n) (equator n) (gp z) = z" ``` lp15@70097 ` 94` ``` using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def) ``` lp15@70097 ` 95` ``` have giso: "gp \ Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) ``` lp15@70097 ` 96` ``` (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0})" ``` lp15@70097 ` 97` ``` by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym) ``` lp15@70097 ` 98` ``` show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} = ``` lp15@70097 ` 99` ``` relative_homology_group n (lsphere n) (equator n)" ``` lp15@70097 ` 100` ``` apply (rule monoid.equality) ``` lp15@70097 ` 101` ``` using giso gp.subgroup_generated_by_image [of "{z}"] zcarr ``` lp15@70097 ` 102` ``` by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff) ``` lp15@70097 ` 103` ``` qed ``` lp15@70097 ` 104` ``` have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0} ``` lp15@70097 ` 105` ``` \ iso (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 106` ``` (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))" ``` lp15@70097 ` 107` ``` using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp ``` lp15@70097 ` 108` ``` then obtain gn where g: "group_isomorphisms ``` lp15@70097 ` 109` ``` (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 110` ``` (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) ``` lp15@70097 ` 111` ``` (hom_boundary n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}) ``` lp15@70097 ` 112` ``` gn" ``` lp15@70097 ` 113` ``` by (auto simp: group.iso_iff_group_isomorphisms) ``` lp15@70097 ` 114` ``` then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" ``` lp15@70097 ` 115` ``` "relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0}" gn ``` lp15@70097 ` 116` ``` by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def) ``` lp15@70097 ` 117` ``` obtain zn where zncarr: "zn \ carrier(relative_homology_group n (usphere n) (equator n))" ``` lp15@70097 ` 118` ``` and zn_z: "hom_boundary n (usphere n) (equator n) zn = z" ``` lp15@70097 ` 119` ``` and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn} ``` lp15@70097 ` 120` ``` = relative_homology_group n (usphere n) (equator n)" ``` lp15@70097 ` 121` ``` proof ``` lp15@70097 ` 122` ``` show "gn z \ carrier (relative_homology_group n (usphere n) (equator n))" ``` lp15@70097 ` 123` ``` "hom_boundary n (usphere n) (equator n) (gn z) = z" ``` lp15@70097 ` 124` ``` using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def) ``` lp15@70097 ` 125` ``` have giso: "gn \ Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) ``` lp15@70097 ` 126` ``` (relative_homology_group n (subtopology (nsphere n) {x. x n \ 0}) {x. x n = 0})" ``` lp15@70097 ` 127` ``` by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym) ``` lp15@70097 ` 128` ``` show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} = ``` lp15@70097 ` 129` ``` relative_homology_group n (usphere n) (equator n)" ``` lp15@70097 ` 130` ``` apply (rule monoid.equality) ``` lp15@70097 ` 131` ``` using giso gn.subgroup_generated_by_image [of "{z}"] zcarr ``` lp15@70097 ` 132` ``` by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff) ``` lp15@70097 ` 133` ``` qed ``` lp15@70097 ` 134` ``` let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id" ``` lp15@70097 ` 135` ``` interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu ``` lp15@70097 ` 136` ``` by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) ``` lp15@70097 ` 137` ``` interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f" ``` lp15@70097 ` 138` ``` by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) ``` lp15@70097 ` 139` ``` define wp where "wp \ ?hi_lu zp" ``` lp15@70097 ` 140` ``` then have wpcarr: "wp \ carrier(?rhgn (upper n))" ``` lp15@70097 ` 141` ``` by (simp add: hom_induced_carrier) ``` lp15@70097 ` 142` ``` have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id ``` lp15@70097 ` 143` ``` \ iso (reduced_homology_group n (nsphere n)) ``` lp15@70097 ` 144` ``` (?rhgn {x. x n \ 0})" ``` lp15@70097 ` 145` ``` using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto ``` lp15@70097 ` 146` ``` then have "carrier(?rhgn {x. x n \ 0}) ``` lp15@70097 ` 147` ``` \ (hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id) ``` lp15@70097 ` 148` ``` ` carrier(reduced_homology_group n (nsphere n))" ``` lp15@70097 ` 149` ``` by (simp add: iso_iff) ``` lp15@70097 ` 150` ``` then obtain vp where vpcarr: "vp \ carrier(reduced_homology_group n (nsphere n))" ``` lp15@70097 ` 151` ``` and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp" ``` lp15@70097 ` 152` ``` using wpcarr by (auto simp: upper_def) ``` lp15@70097 ` 153` ``` define wn where "wn \ hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn" ``` lp15@70097 ` 154` ``` then have wncarr: "wn \ carrier(?rhgn (lower n))" ``` lp15@70097 ` 155` ``` by (simp add: hom_induced_carrier) ``` lp15@70097 ` 156` ``` have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id ``` lp15@70097 ` 157` ``` \ iso (reduced_homology_group n (nsphere n)) ``` lp15@70097 ` 158` ``` (?rhgn {x. x n \ 0})" ``` lp15@70097 ` 159` ``` using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto ``` lp15@70097 ` 160` ``` then have "carrier(?rhgn {x. x n \ 0}) ``` lp15@70097 ` 161` ``` \ (hom_induced n (nsphere n) {} (nsphere n) {x. x n \ 0} id) ``` lp15@70097 ` 162` ``` ` carrier(reduced_homology_group n (nsphere n))" ``` lp15@70097 ` 163` ``` by (simp add: iso_iff) ``` lp15@70097 ` 164` ``` then obtain vn where vpcarr: "vn \ carrier(reduced_homology_group n (nsphere n))" ``` lp15@70097 ` 165` ``` and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn" ``` lp15@70097 ` 166` ``` using wncarr by (auto simp: lower_def) ``` lp15@70097 ` 167` ``` define up where "up \ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp" ``` lp15@70097 ` 168` ``` then have upcarr: "up \ carrier(?rhgn (equator n))" ``` lp15@70097 ` 169` ``` by (simp add: hom_induced_carrier) ``` lp15@70097 ` 170` ``` define un where "un \ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn" ``` lp15@70097 ` 171` ``` then have uncarr: "un \ carrier(?rhgn (equator n))" ``` lp15@70097 ` 172` ``` by (simp add: hom_induced_carrier) ``` lp15@70097 ` 173` ``` have *: "(\(x, y). ``` lp15@70097 ` 174` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x ``` lp15@70097 ` 175` ``` \\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 176` ``` hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y) ``` lp15@70097 ` 177` ``` \ Group.iso ``` lp15@70097 ` 178` ``` (relative_homology_group n (lsphere n) (equator n) \\ ``` lp15@70097 ` 179` ``` relative_homology_group n (usphere n) (equator n)) ``` lp15@70097 ` 180` ``` (?rhgn (equator n))" ``` lp15@70097 ` 181` ``` proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]]) ``` lp15@70097 ` 182` ``` show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id ``` lp15@70097 ` 183` ``` \ Group.iso (relative_homology_group n (lsphere n) (equator n)) ``` lp15@70097 ` 184` ``` (?rhgn (upper n))" ``` lp15@70097 ` 185` ``` apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def) ``` lp15@70097 ` 186` ``` using iso_relative_homology_group_lower_hemisphere by blast ``` lp15@70097 ` 187` ``` show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id ``` lp15@70097 ` 188` ``` \ Group.iso (relative_homology_group n (usphere n) (equator n)) ``` lp15@70097 ` 189` ``` (?rhgn (lower n))" ``` lp15@70097 ` 190` ``` apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def) ``` lp15@70097 ` 191` ``` using iso_relative_homology_group_upper_hemisphere by blast+ ``` lp15@70097 ` 192` ``` show "exact_seq ``` lp15@70097 ` 193` ``` ([?rhgn (lower n), ``` lp15@70097 ` 194` ``` ?rhgn (equator n), ``` lp15@70097 ` 195` ``` relative_homology_group n (lsphere n) (equator n)], ``` lp15@70097 ` 196` ``` [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id, ``` lp15@70097 ` 197` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])" ``` lp15@70097 ` 198` ``` unfolding lsphere_def usphere_def equator_def lower_def upper_def ``` lp15@70097 ` 199` ``` by (rule homology_exactness_triple_3) force ``` lp15@70097 ` 200` ``` show "exact_seq ``` lp15@70097 ` 201` ``` ([?rhgn (upper n), ``` lp15@70097 ` 202` ``` ?rhgn (equator n), ``` lp15@70097 ` 203` ``` relative_homology_group n (usphere n) (equator n)], ``` lp15@70097 ` 204` ``` [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id, ``` lp15@70097 ` 205` ``` hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])" ``` lp15@70097 ` 206` ``` unfolding lsphere_def usphere_def equator_def lower_def upper_def ``` lp15@70097 ` 207` ``` by (rule homology_exactness_triple_3) force ``` lp15@70097 ` 208` ``` next ``` lp15@70097 ` 209` ``` fix x ``` lp15@70097 ` 210` ``` assume "x \ carrier (relative_homology_group n (lsphere n) (equator n))" ``` lp15@70097 ` 211` ``` show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id ``` lp15@70097 ` 212` ``` (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) = ``` lp15@70097 ` 213` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x" ``` lp15@70097 ` 214` ``` by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def) ``` lp15@70097 ` 215` ``` next ``` lp15@70097 ` 216` ``` fix x ``` lp15@70097 ` 217` ``` assume "x \ carrier (relative_homology_group n (usphere n) (equator n))" ``` lp15@70097 ` 218` ``` show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id ``` lp15@70097 ` 219` ``` (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) = ``` lp15@70097 ` 220` ``` hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x" ``` lp15@70097 ` 221` ``` by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def) ``` lp15@70097 ` 222` ``` qed ``` lp15@70097 ` 223` ``` then have sb: "carrier (?rhgn (equator n)) ``` lp15@70097 ` 224` ``` \ (\(x, y). ``` lp15@70097 ` 225` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x ``` lp15@70097 ` 226` ``` \\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 227` ``` hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y) ``` lp15@70097 ` 228` ``` ` carrier (relative_homology_group n (lsphere n) (equator n) \\ ``` lp15@70097 ` 229` ``` relative_homology_group n (usphere n) (equator n))" ``` lp15@70097 ` 230` ``` by (simp add: iso_iff) ``` lp15@70097 ` 231` ``` obtain a b::int ``` lp15@70097 ` 232` ``` where up_ab: "?hi_ee f up ``` lp15@70097 ` 233` ``` = up [^]\<^bsub>?rhgn (equator n)\<^esub> a\\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b" ``` lp15@70097 ` 234` ``` proof - ``` lp15@70097 ` 235` ``` have hiupcarr: "?hi_ee f up \ carrier(?rhgn (equator n))" ``` lp15@70097 ` 236` ``` by (simp add: hom_induced_carrier) ``` lp15@70097 ` 237` ``` obtain u v where u: "u \ carrier (relative_homology_group n (lsphere n) (equator n))" ``` lp15@70097 ` 238` ``` and v: "v \ carrier (relative_homology_group n (usphere n) (equator n))" ``` lp15@70097 ` 239` ``` and eq: "?hi_ee f up = ``` lp15@70097 ` 240` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u ``` lp15@70097 ` 241` ``` \\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 242` ``` hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v" ``` lp15@70097 ` 243` ``` using subsetD [OF sb hiupcarr] by auto ``` lp15@70097 ` 244` ``` have "u \ carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})" ``` lp15@70097 ` 245` ``` by (simp_all add: u zp_sg) ``` lp15@70097 ` 246` ``` then obtain a::int where a: "u = zp [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> a" ``` lp15@70097 ` 247` ``` by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr) ``` lp15@70097 ` 248` ``` have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id ``` lp15@70097 ` 249` ``` (pow (relative_homology_group n (lsphere n) (equator n)) zp a) ``` lp15@70097 ` 250` ``` = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a" ``` lp15@70097 ` 251` ``` by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr) ``` lp15@70097 ` 252` ``` have "v \ carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})" ``` lp15@70097 ` 253` ``` by (simp_all add: v zn_sg) ``` lp15@70097 ` 254` ``` then obtain b::int where b: "v = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b" ``` lp15@70097 ` 255` ``` by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr) ``` lp15@70097 ` 256` ``` have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id ``` lp15@70097 ` 257` ``` (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b) ``` lp15@70097 ` 258` ``` = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id ``` lp15@70097 ` 259` ``` zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b" ``` lp15@70097 ` 260` ``` by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr) ``` lp15@70097 ` 261` ``` show thesis ``` lp15@70097 ` 262` ``` proof ``` lp15@70097 ` 263` ``` show "?hi_ee f up ``` lp15@70097 ` 264` ``` = up [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b" ``` lp15@70097 ` 265` ``` using a ae b be eq local.up_def un_def by auto ``` lp15@70097 ` 266` ``` qed ``` lp15@70097 ` 267` ``` qed ``` lp15@70097 ` 268` ``` have "(hom_boundary n (nsphere n) (equator n) ``` lp15@70097 ` 269` ``` \ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z" ``` lp15@70097 ` 270` ``` using zp_z equ apply (simp add: lsphere_def naturality_hom_induced) ``` lp15@70097 ` 271` ``` by (metis hom_boundary_carrier hom_induced_id) ``` lp15@70097 ` 272` ``` then have up_z: "hom_boundary n (nsphere n) (equator n) up = z" ``` lp15@70097 ` 273` ``` by (simp add: up_def) ``` lp15@70097 ` 274` ``` have "(hom_boundary n (nsphere n) (equator n) ``` lp15@70097 ` 275` ``` \ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z" ``` lp15@70097 ` 276` ``` using zn_z equ apply (simp add: usphere_def naturality_hom_induced) ``` lp15@70097 ` 277` ``` by (metis hom_boundary_carrier hom_induced_id) ``` lp15@70097 ` 278` ``` then have un_z: "hom_boundary n (nsphere n) (equator n) un = z" ``` lp15@70097 ` 279` ``` by (simp add: un_def) ``` lp15@70097 ` 280` ``` have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b" ``` lp15@70097 ` 281` ``` proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all) ``` lp15@70097 ` 282` ``` show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f" ``` lp15@70097 ` 283` ``` using cmr by auto ``` lp15@70097 ` 284` ``` show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} = ``` lp15@70097 ` 285` ``` reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" ``` lp15@70097 ` 286` ``` using zeq by blast ``` lp15@70097 ` 287` ``` have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f ``` lp15@70097 ` 288` ``` \ hom_boundary n (nsphere n) (equator n)) up ``` lp15@70097 ` 289` ``` = (hom_boundary n (nsphere n) (equator n) \ ``` lp15@70097 ` 290` ``` ?hi_ee f) up" ``` lp15@70097 ` 291` ``` using naturality_hom_induced [OF cmf fimeq, of n, symmetric] ``` lp15@70097 ` 292` ``` by (simp add: subtopology_restrict equ fun_eq_iff) ``` lp15@70097 ` 293` ``` also have "\ = hom_boundary n (nsphere n) (equator n) ``` lp15@70097 ` 294` ``` (up [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> ``` lp15@70097 ` 295` ``` a \\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> ``` lp15@70097 ` 296` ``` un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)" ``` lp15@70097 ` 297` ``` by (simp add: o_def up_ab) ``` lp15@70097 ` 298` ``` also have "\ = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)" ``` lp15@70097 ` 299` ``` using zcarr ``` lp15@70097 ` 300` ``` apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr) ``` lp15@70097 ` 301` ``` by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z) ``` lp15@70097 ` 302` ``` finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z = ``` lp15@70097 ` 303` ``` z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)" ``` lp15@70097 ` 304` ``` by (simp add: up_z) ``` lp15@70097 ` 305` ``` qed ``` lp15@70097 ` 306` ``` define u where "u \ up \\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un" ``` lp15@70097 ` 307` ``` have ucarr: "u \ carrier (?rhgn (equator n))" ``` lp15@70097 ` 308` ``` by (simp add: u_def uncarr upcarr) ``` lp15@70097 ` 309` ``` then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b) ``` lp15@70097 ` 310` ``` \ (GE.ord u) dvd a - b - Brouwer_degree2 n f" ``` lp15@70097 ` 311` ``` by (simp add: GE.int_pow_eq) ``` lp15@70097 ` 312` ``` moreover ``` lp15@70097 ` 313` ``` have "GE.ord u = 0" ``` lp15@70097 ` 314` ``` proof (clarsimp simp add: GE.ord_eq_0 ucarr) ``` lp15@70097 ` 315` ``` fix d :: nat ``` lp15@70097 ` 316` ``` assume "0 < d" ``` lp15@70097 ` 317` ``` and "u [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)" ``` lp15@70097 ` 318` ``` then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d ``` lp15@70097 ` 319` ``` = \\<^bsub>?rhgn (upper n)\<^esub>" ``` lp15@70097 ` 320` ``` by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr) ``` lp15@70097 ` 321` ``` moreover ``` lp15@70097 ` 322` ``` have "?hi_lu ``` lp15@70097 ` 323` ``` = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id \ ``` lp15@70097 ` 324` ``` hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id" ``` lp15@70097 ` 325` ``` by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose) ``` lp15@70097 ` 326` ``` then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up" ``` lp15@70097 ` 327` ``` by (simp add: local.up_def wp_def) ``` lp15@70097 ` 328` ``` have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = \\<^bsub>?rhgn (upper n)\<^esub>" ``` lp15@70097 ` 329` ``` using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"] ``` lp15@70097 ` 330` ``` using un_def zncarr by (auto simp: upper_usphere kernel_def) ``` lp15@70097 ` 331` ``` have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp" ``` lp15@70097 ` 332` ``` unfolding u_def ``` lp15@70097 ` 333` ``` using p n HIU.inv_one HIU.r_one uncarr upcarr by auto ``` lp15@70097 ` 334` ``` ultimately have "(wp [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \\<^bsub>?rhgn (upper n)\<^esub>" ``` lp15@70097 ` 335` ``` by simp ``` lp15@70097 ` 336` ``` moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))" ``` lp15@70097 ` 337` ``` proof - ``` lp15@70097 ` 338` ``` have "?rhgn (upper n) \ reduced_homology_group n (nsphere n)" ``` lp15@70097 ` 339` ``` unfolding upper_def ``` lp15@70097 ` 340` ``` using iso_reduced_homology_group_upper_hemisphere [of n n n] ``` lp15@70097 ` 341` ``` by (blast intro: group.iso_sym group_reduced_homology_group is_isoI) ``` lp15@70097 ` 342` ``` also have "\ \ integer_group" ``` lp15@70097 ` 343` ``` by (simp add: reduced_homology_group_nsphere) ``` lp15@70097 ` 344` ``` finally have iso: "?rhgn (upper n) \ integer_group" . ``` lp15@70097 ` 345` ``` have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))" ``` lp15@70097 ` 346` ``` using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset ``` lp15@70097 ` 347` ``` gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg ``` lp15@70097 ` 348` ``` by (auto simp: lower_def lsphere_def upper_def equator_def wp_def) ``` lp15@70097 ` 349` ``` then show ?thesis ``` lp15@70097 ` 350` ``` using infinite_UNIV_int iso_finite [OF iso] by simp ``` lp15@70097 ` 351` ``` qed ``` lp15@70097 ` 352` ``` ultimately show False ``` lp15@70097 ` 353` ``` using HIU.finite_cyclic_subgroup \0 < d\ wpcarr by blast ``` lp15@70097 ` 354` ``` qed ``` lp15@70097 ` 355` ``` ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b) ``` lp15@70097 ` 356` ``` \ Brouwer_degree2 n f = a - b" ``` lp15@70097 ` 357` ``` by auto ``` lp15@70097 ` 358` ``` have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u" ``` lp15@70097 ` 359` ``` proof - ``` lp15@70097 ` 360` ``` have ne: "topspace (nsphere n) \ equator n \ {}" ``` lp15@70097 ` 361` ``` by (metis equ(1) nonempty_nsphere topspace_subtopology) ``` lp15@70097 ` 362` ``` have eq1: "hom_boundary n (nsphere n) (equator n) u ``` lp15@70097 ` 363` ``` = \\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>" ``` lp15@70097 ` 364` ``` using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force ``` lp15@70097 ` 365` ``` then have uhom: "u \ hom_induced n (nsphere n) {} (nsphere n) (equator n) id ` ``` lp15@70097 ` 366` ``` carrier (reduced_homology_group (int n) (nsphere n))" ``` lp15@70097 ` 367` ``` using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def) ``` lp15@70097 ` 368` ``` then obtain v where vcarr: "v \ carrier (reduced_homology_group (int n) (nsphere n))" ``` lp15@70097 ` 369` ``` and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v" ``` lp15@70097 ` 370` ``` by blast ``` lp15@70097 ` 371` ``` interpret GH_hi: group_hom "homology_group n (nsphere n)" ``` lp15@70097 ` 372` ``` "?rhgn (equator n)" ``` lp15@70097 ` 373` ``` "hom_induced n (nsphere n) {} (nsphere n) (equator n) id" ``` lp15@70097 ` 374` ``` by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) ``` lp15@70097 ` 375` ``` have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i" ``` lp15@70097 ` 376` ``` for x and i::int ``` lp15@70097 ` 377` ``` by (simp add: False un_reduced_homology_group) ``` lp15@70097 ` 378` ``` have vcarr': "v \ carrier (homology_group n (nsphere n))" ``` lp15@70097 ` 379` ``` using carrier_reduced_homology_group_subset vcarr by blast ``` lp15@70097 ` 380` ``` have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f ``` lp15@70097 ` 381` ``` = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v" ``` lp15@70097 ` 382` ``` using vcarr vcarr' ``` lp15@70097 ` 383` ``` by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2) ``` lp15@70097 ` 384` ``` also have "\ = hom_induced n (nsphere n) (topspace(nsphere n) \ equator n) (nsphere n) (equator n) f ``` lp15@70097 ` 385` ``` (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \ equator n) id v)" ``` lp15@70097 ` 386` ``` using fimeq by (simp add: hom_induced_compose' cmf) ``` lp15@70097 ` 387` ``` also have "\ = ?hi_ee f u" ``` lp15@70097 ` 388` ``` by (metis hom_induced inf.left_idem ueq) ``` lp15@70097 ` 389` ``` finally show ?thesis . ``` lp15@70097 ` 390` ``` qed ``` lp15@70097 ` 391` ``` moreover ``` lp15@70097 ` 392` ``` interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg" ``` lp15@70097 ` 393` ``` by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom) ``` lp15@70097 ` 394` ``` have hi_up_eq_un: "?hi_ee neg up = un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" ``` lp15@70097 ` 395` ``` proof - ``` lp15@70097 ` 396` ``` have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) ``` lp15@70097 ` 397` ``` = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg \ id) zp" ``` lp15@70097 ` 398` ``` by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg) ``` lp15@70097 ` 399` ``` also have "\ = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id ``` lp15@70097 ` 400` ``` (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)" ``` lp15@70097 ` 401` ``` by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def) ``` lp15@70097 ` 402` ``` also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp ``` lp15@70097 ` 403` ``` = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" ``` lp15@70097 ` 404` ``` proof - ``` lp15@70097 ` 405` ``` let ?hb = "hom_boundary n (usphere n) (equator n)" ``` lp15@70097 ` 406` ``` have eq: "subtopology (nsphere n) {x. x n \ 0} = usphere n \ {x. x n = 0} = equator n" ``` lp15@70097 ` 407` ``` by (auto simp: usphere_def upper_def equator_def) ``` lp15@70097 ` 408` ``` with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))" ``` lp15@70097 ` 409` ``` by (simp add: iso_iff) ``` lp15@70097 ` 410` ``` interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)" ``` lp15@70097 ` 411` ``` "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))" ``` lp15@70097 ` 412` ``` "?hb" ``` lp15@70097 ` 413` ``` using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce ``` lp15@70097 ` 414` ``` show ?thesis ``` lp15@70097 ` 415` ``` proof (rule inj_onD [OF inj]) ``` lp15@70097 ` 416` ``` have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z ``` lp15@70097 ` 417` ``` = z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg" ``` lp15@70097 ` 418` ``` using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr ``` lp15@70097 ` 419` ``` by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def) ``` lp15@70097 ` 420` ``` have "?hb \ ``` lp15@70097 ` 421` ``` hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg ``` lp15@70097 ` 422` ``` = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg \ ``` lp15@70097 ` 423` ``` hom_boundary n (lsphere n) (equator n)" ``` lp15@70097 ` 424` ``` apply (subst naturality_hom_induced [OF cm_neg_lu]) ``` lp15@70097 ` 425` ``` apply (force simp: equator_def neg_def) ``` lp15@70097 ` 426` ``` by (simp add: equ) ``` lp15@70097 ` 427` ``` then have "?hb ``` lp15@70097 ` 428` ``` (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) ``` lp15@70097 ` 429` ``` = (z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)" ``` lp15@70097 ` 430` ``` by (metis "*" comp_apply zp_z) ``` lp15@70097 ` 431` ``` also have "\ = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> ``` lp15@70097 ` 432` ``` Brouwer_degree2 (n - Suc 0) neg)" ``` lp15@70097 ` 433` ``` by (metis group.int_pow_subgroup_generated group_relative_homology_group hb_hom.hom_int_pow reduced_homology_group_def zcarr zn_z zncarr) ``` lp15@70097 ` 434` ``` finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) = ``` lp15@70097 ` 435` ``` ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> ``` lp15@70097 ` 436` ``` Brouwer_degree2 (n - Suc 0) neg)" by simp ``` lp15@70097 ` 437` ``` qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr) ``` lp15@70097 ` 438` ``` qed ``` lp15@70097 ` 439` ``` finally show ?thesis ``` lp15@70097 ` 440` ``` by (metis (no_types, lifting) group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced local.up_def un_def zncarr) ``` lp15@70097 ` 441` ``` qed ``` lp15@70097 ` 442` ``` have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg" ``` lp15@70097 ` 443` ``` using cm_neg by blast ``` lp15@70097 ` 444` ``` then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg" ``` lp15@70097 ` 445` ``` apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def) ``` lp15@70097 ` 446` ``` apply (rule_tac x=neg in exI, auto) ``` lp15@70097 ` 447` ``` done ``` lp15@70097 ` 448` ``` then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1" ``` lp15@70097 ` 449` ``` using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force ``` lp15@70097 ` 450` ``` have hi_un_eq_up: "?hi_ee neg un = up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" (is "?f un = ?y") ``` lp15@70097 ` 451` ``` proof - ``` lp15@70097 ` 452` ``` have [simp]: "neg \ neg = id" ``` lp15@70097 ` 453` ``` by force ``` lp15@70097 ` 454` ``` have "?f (?f ?y) = ?y" ``` lp15@70097 ` 455` ``` apply (subst hom_induced_compose' [OF cm_neg _ cm_neg]) ``` lp15@70097 ` 456` ``` apply(force simp: equator_def) ``` lp15@70097 ` 457` ``` apply (simp add: upcarr hom_induced_id_gen) ``` lp15@70097 ` 458` ``` done ``` lp15@70097 ` 459` ``` moreover have "?f ?y = un" ``` lp15@70097 ` 460` ``` using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un) ``` lp15@70097 ` 461` ``` by (metis (no_types, lifting) Brouwer_degree2_21 GE.group_l_invI GE.l_inv_ex group.int_pow_1 group.int_pow_pow power2_eq_1_iff uncarr zmult_eq_1_iff) ``` lp15@70097 ` 462` ``` ultimately show "?f un = ?y" ``` lp15@70097 ` 463` ``` by simp ``` lp15@70097 ` 464` ``` qed ``` lp15@70097 ` 465` ``` have "?hi_ee f un = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b" ``` lp15@70097 ` 466` ``` proof - ``` lp15@70097 ` 467` ``` let ?TE = "topspace (nsphere n) \ equator n" ``` lp15@70097 ` 468` ``` have fneg: "(f \ neg) x = (neg \ f) x" if "x \ topspace (nsphere n)" for x ``` lp15@70097 ` 469` ``` using f [OF that] by (force simp: neg_def) ``` lp15@70097 ` 470` ``` have neg_im: "neg ` (topspace (nsphere n) \ equator n) \ topspace (nsphere n) \ equator n" ``` lp15@70097 ` 471` ``` by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology) ``` lp15@70097 ` 472` ``` have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \ hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg ``` lp15@70097 ` 473` ``` = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \ hom_induced n (nsphere n) ?TE (nsphere n) ?TE f" ``` lp15@70097 ` 474` ``` using neg_im fimeq cm_neg cmf ``` lp15@70097 ` 475` ``` apply (simp add: flip: hom_induced_compose del: hom_induced_restrict) ``` lp15@70097 ` 476` ``` using fneg by (auto intro: hom_induced_eq) ``` lp15@70097 ` 477` ``` have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b) ``` lp15@70097 ` 478` ``` = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg) ``` lp15@70097 ` 479` ``` \\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 480` ``` up [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)" ``` lp15@70097 ` 481` ``` proof - ``` lp15@70097 ` 482` ``` have "Brouwer_degree2 (n - Suc 0) neg = 1 \ Brouwer_degree2 (n - Suc 0) neg = - 1" ``` lp15@70097 ` 483` ``` using Brouwer_degree2_21 power2_eq_1_iff by blast ``` lp15@70097 ` 484` ``` then show ?thesis ``` lp15@70097 ` 485` ``` by fastforce ``` lp15@70097 ` 486` ``` qed ``` lp15@70097 ` 487` ``` also have "\ = ((un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 488` ``` (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub> ``` lp15@70097 ` 489` ``` Brouwer_degree2 (n - 1) neg" ``` lp15@70097 ` 490` ``` by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr) ``` lp15@70097 ` 491` ``` also have "\ = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" ``` lp15@70097 ` 492` ``` by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr) ``` lp15@70097 ` 493` ``` finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b) ``` lp15@70097 ` 494` ``` = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" . ``` lp15@70097 ` 495` ``` have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" ``` lp15@70097 ` 496` ``` by (metis (no_types, hide_lams) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff) ``` lp15@70097 ` 497` ``` moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg)) ``` lp15@70097 ` 498` ``` = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b" ``` lp15@70097 ` 499` ``` using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff) ``` lp15@70097 ` 500` ``` ultimately show ?thesis ``` lp15@70097 ` 501` ``` by blast ``` lp15@70097 ` 502` ``` qed ``` lp15@70097 ` 503` ``` then have "?hi_ee f u = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)" ``` lp15@70097 ` 504` ``` by (simp add: u_def upcarr uncarr up_ab GE.int_pow_diff GE.m_ac GE.int_pow_distrib GE.int_pow_inv GE.inv_mult_group) ``` lp15@70097 ` 505` ``` ultimately ``` lp15@70097 ` 506` ``` have "Brouwer_degree2 n f = a - b" ``` lp15@70097 ` 507` ``` using iff by blast ``` lp15@70097 ` 508` ``` with Bd_ab show ?thesis ``` lp15@70097 ` 509` ``` by simp ``` lp15@70097 ` 510` ```qed simp ``` lp15@70097 ` 511` lp15@70097 ` 512` lp15@70097 ` 513` ```subsection \General Jordan-Brouwer separation theorem and invariance of dimension\ ``` lp15@70097 ` 514` lp15@70097 ` 515` ```proposition relative_homology_group_Euclidean_complement_step: ``` lp15@70097 ` 516` ``` assumes "closedin (Euclidean_space n) S" ``` lp15@70097 ` 517` ``` shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S) ``` lp15@70097 ` 518` ``` \ relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)" ``` lp15@70097 ` 519` ```proof - ``` lp15@70097 ` 520` ``` have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S) ``` lp15@70097 ` 521` ``` \ relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \ S. x n = 0})" ``` lp15@70097 ` 522` ``` (is "?lhs \ ?rhs") ``` lp15@70097 ` 523` ``` if clo: "closedin (Euclidean_space (Suc n)) S" and cong: "\x y. \x \ S; \i. i \ n \ x i = y i\ \ y \ S" ``` lp15@70097 ` 524` ``` for p n S ``` lp15@70097 ` 525` ``` proof - ``` lp15@70097 ` 526` ``` have Ssub: "S \ topspace (Euclidean_space (Suc n))" ``` lp15@70097 ` 527` ``` by (meson clo closedin_def) ``` lp15@70097 ` 528` ``` define lo where "lo \ {x \ topspace(Euclidean_space (Suc n)). x n < (if x \ S then 0 else 1)}" ``` lp15@70097 ` 529` ``` define hi where "hi = {x \ topspace(Euclidean_space (Suc n)). x n > (if x \ S then 0 else -1)}" ``` lp15@70097 ` 530` ``` have lo_hi_Int: "lo \ hi = {x \ topspace(Euclidean_space (Suc n)) - S. x n \ {-1<..<1}}" ``` lp15@70097 ` 531` ``` by (auto simp: hi_def lo_def) ``` lp15@70097 ` 532` ``` have lo_hi_Un: "lo \ hi = topspace(Euclidean_space (Suc n)) - {x \ S. x n = 0}" ``` lp15@70097 ` 533` ``` by (auto simp: hi_def lo_def) ``` lp15@70097 ` 534` ``` define ret where "ret \ \c::real. \x i. if i = n then c else x i" ``` lp15@70097 ` 535` ``` have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t ``` lp15@70097 ` 536` ``` by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection) ``` lp15@70097 ` 537` ``` let ?ST = "\t. subtopology (Euclidean_space (Suc n)) {x. x n = t}" ``` lp15@70097 ` 538` ``` define squashable where ``` lp15@70097 ` 539` ``` "squashable \ \t S. \x t'. x \ S \ (x n \ t' \ t' \ t \ t \ t' \ t' \ x n) \ ret t' x \ S" ``` lp15@70097 ` 540` ``` have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t ``` lp15@70097 ` 541` ``` by (simp add: squashable_def topspace_Euclidean_space ret_def) ``` lp15@70097 ` 542` ``` have squashableD: "\squashable t S; x \ S; x n \ t' \ t' \ t \ t \ t' \ t' \ x n\ \ ret t' x \ S" for x t' t S ``` lp15@70097 ` 543` ``` by (auto simp: squashable_def) ``` lp15@70097 ` 544` ``` have "squashable 1 hi" ``` lp15@70097 ` 545` ``` by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong) ``` lp15@70097 ` 546` ``` have "squashable t UNIV" for t ``` lp15@70097 ` 547` ``` by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong) ``` lp15@70097 ` 548` ``` have squashable_0_lohi: "squashable 0 (lo \ hi)" ``` lp15@70097 ` 549` ``` using Ssub ``` lp15@70097 ` 550` ``` by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong) ``` lp15@70097 ` 551` ``` have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U) ``` lp15@70097 ` 552` ``` (subtopology (Euclidean_space (Suc n)) {x. x \ U \ x n = t}) ``` lp15@70097 ` 553` ``` (ret t) id" ``` lp15@70097 ` 554` ``` if "squashable t U" for t U ``` lp15@70097 ` 555` ``` unfolding retraction_maps_def ``` lp15@70097 ` 556` ``` proof (intro conjI ballI) ``` lp15@70097 ` 557` ``` show "continuous_map (subtopology (Euclidean_space (Suc n)) U) ``` lp15@70097 ` 558` ``` (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t}) (ret t)" ``` lp15@70097 ` 559` ``` apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def) ``` lp15@70097 ` 560` ``` using that by (fastforce simp: squashable_def ret_def) ``` lp15@70097 ` 561` ``` next ``` lp15@70097 ` 562` ``` show "continuous_map (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t}) ``` lp15@70097 ` 563` ``` (subtopology (Euclidean_space (Suc n)) U) id" ``` lp15@70097 ` 564` ``` using continuous_map_in_subtopology by fastforce ``` lp15@70097 ` 565` ``` show "ret t (id x) = x" ``` lp15@70097 ` 566` ``` if "x \ topspace (subtopology (Euclidean_space (Suc n)) {x \ U. x n = t})" for x ``` lp15@70097 ` 567` ``` using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff) ``` lp15@70097 ` 568` ``` qed ``` lp15@70097 ` 569` ``` have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S)) ``` lp15@70097 ` 570` ``` euclideanreal (\x. snd x k)" for k::nat and S ``` lp15@70097 ` 571` ``` using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce ``` lp15@70097 ` 572` ``` have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S)) ``` lp15@70097 ` 573` ``` euclideanreal (\x. fst x * snd x k)" for k::nat and S ``` lp15@70097 ` 574` ``` by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd) ``` lp15@70097 ` 575` ``` have hw_sub: "homotopic_with (\k. k ` V \ V) (subtopology (Euclidean_space (Suc n)) U) ``` lp15@70097 ` 576` ``` (subtopology (Euclidean_space (Suc n)) U) (ret t) id" ``` lp15@70097 ` 577` ``` if "squashable t U" "squashable t V" for U V t ``` lp15@70097 ` 578` ``` unfolding homotopic_with_def ``` lp15@70097 ` 579` ``` proof (intro exI conjI allI ballI) ``` lp15@70097 ` 580` ``` let ?h = "\(z,x). ret ((1 - z) * t + z * x n) x" ``` lp15@70097 ` 581` ``` show "(\x. ?h (u, x)) ` V \ V" if "u \ {0..1}" for u ``` lp15@70097 ` 582` ``` using that ``` lp15@70097 ` 583` ``` by clarsimp (metis squashableD [OF \squashable t V\] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma) ``` lp15@70097 ` 584` ``` have 1: "?h ` ({0..1} \ ({x. \i\Suc n. x i = 0} \ U)) \ U" ``` lp15@70097 ` 585` ``` by clarsimp (metis squashableD [OF \squashable t U\] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma) ``` lp15@70097 ` 586` ``` show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U)) ``` lp15@70097 ` 587` ``` (subtopology (Euclidean_space (Suc n)) U) ?h" ``` lp15@70097 ` 588` ``` apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1) ``` lp15@70097 ` 589` ``` apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV) ``` lp15@70097 ` 590` ``` apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros) ``` lp15@70097 ` 591` ``` by (auto simp: cm_snd) ``` lp15@70097 ` 592` ``` qed (auto simp: ret_def) ``` lp15@70097 ` 593` ``` have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)" ``` lp15@70097 ` 594` ``` proof - ``` lp15@70097 ` 595` ``` have "homotopic_with (\x. True) (?ST 1) (?ST 1) id (\x. (\i. if i = n then 1 else 0))" ``` lp15@70097 ` 596` ``` apply (subst homotopic_with_sym) ``` lp15@70097 ` 597` ``` apply (simp add: homotopic_with) ``` lp15@70097 ` 598` ``` apply (rule_tac x="(\(z,x) i. if i=n then 1 else z * x i)" in exI) ``` lp15@70097 ` 599` ``` apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd) ``` lp15@70097 ` 600` ``` done ``` lp15@70097 ` 601` ``` then have "contractible_space (?ST 1)" ``` lp15@70097 ` 602` ``` unfolding contractible_space_def by metis ``` lp15@70097 ` 603` ``` moreover have "?thesis = contractible_space (?ST 1)" ``` lp15@70097 ` 604` ``` proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility) ``` lp15@70097 ` 605` ``` have "{x. \i\Suc n. x i = 0} \ {x \ hi. x n = 1} = {x. \i\Suc n. x i = 0} \ {x. x n = 1}" ``` lp15@70097 ` 606` ``` by (auto simp: hi_def topspace_Euclidean_space) ``` lp15@70097 ` 607` ``` then have eq: "subtopology (Euclidean_space (Suc n)) {x. x \ hi \ x n = 1} = ?ST 1" ``` lp15@70097 ` 608` ``` by (simp add: Euclidean_space_def subtopology_subtopology) ``` lp15@70097 ` 609` ``` show "homotopic_with (\x. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id" ``` lp15@70097 ` 610` ``` using hw_sub [OF \squashable 1 hi\ \squashable 1 UNIV\] eq by simp ``` lp15@70097 ` 611` ``` show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id" ``` lp15@70097 ` 612` ``` using rm_ret [OF \squashable 1 hi\] eq by simp ``` lp15@70097 ` 613` ``` qed ``` lp15@70097 ` 614` ``` ultimately show ?thesis by metis ``` lp15@70097 ` 615` ``` qed ``` lp15@70097 ` 616` ``` have "?lhs \ relative_homology_group p (Euclidean_space (Suc n)) (lo \ hi)" ``` lp15@70097 ` 617` ``` proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups]) ``` lp15@70097 ` 618` ``` have "{x. \i\Suc n. x i = 0} \ {x. x n = 0} = {x. \i\n. x i = (0::real)}" ``` lp15@70097 ` 619` ``` by auto (metis le_less_Suc_eq not_le) ``` lp15@70097 ` 620` ``` then have "?ST 0 = Euclidean_space n" ``` lp15@70097 ` 621` ``` by (simp add: Euclidean_space_def subtopology_subtopology) ``` lp15@70097 ` 622` ``` then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id" ``` lp15@70097 ` 623` ``` using rm_ret [OF \squashable 0 UNIV\] by auto ``` lp15@70097 ` 624` ``` then have "ret 0 x \ topspace (Euclidean_space n)" ``` lp15@70097 ` 625` ``` if "x \ topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x ``` lp15@70097 ` 626` ``` using that by (simp add: continuous_map_def retraction_maps_def) ``` lp15@70097 ` 627` ``` then show "(ret 0) ` (lo \ hi) \ topspace (Euclidean_space n) - S" ``` lp15@70097 ` 628` ``` by (auto simp: local.cong ret_def hi_def lo_def) ``` lp15@70097 ` 629` ``` show "homotopic_with (\h. h ` (lo \ hi) \ lo \ hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id" ``` lp15@70097 ` 630` ``` using hw_sub [OF squashable squashable_0_lohi] by simp ``` lp15@70097 ` 631` ``` qed (auto simp: lo_def hi_def Euclidean_space_def) ``` lp15@70097 ` 632` ``` also have "\ \ relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo \ hi)" ``` lp15@70097 ` 633` ``` proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible]) ``` lp15@70097 ` 634` ``` show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)" ``` lp15@70097 ` 635` ``` by (simp add: cs_hi) ``` lp15@70097 ` 636` ``` show "topspace (Euclidean_space (Suc n)) \ hi \ {}" ``` lp15@70097 ` 637` ``` apply (simp add: hi_def topspace_Euclidean_space set_eq_iff) ``` lp15@70097 ` 638` ``` apply (rule_tac x="\i. if i = n then 1 else 0" in exI, auto) ``` lp15@70097 ` 639` ``` done ``` lp15@70097 ` 640` ``` qed auto ``` lp15@70097 ` 641` ``` also have "\ \ relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo \ hi)) lo" ``` lp15@70097 ` 642` ``` proof - ``` lp15@70097 ` 643` ``` have oo: "openin (Euclidean_space (Suc n)) {x \ topspace (Euclidean_space (Suc n)). x n \ A}" ``` lp15@70097 ` 644` ``` if "open A" for A ``` lp15@70097 ` 645` ``` proof (rule openin_continuous_map_preimage) ``` lp15@70097 ` 646` ``` show "continuous_map (Euclidean_space (Suc n)) euclideanreal (\x. x n)" ``` lp15@70097 ` 647` ``` proof - ``` lp15@70097 ` 648` ``` have "\n f. continuous_map (product_topology f UNIV) (f (n::nat)) (\f. f n::real)" ``` lp15@70097 ` 649` ``` by (simp add: continuous_map_product_projection) ``` lp15@70097 ` 650` ``` then show ?thesis ``` lp15@70097 ` 651` ``` using Euclidean_space_def continuous_map_from_subtopology ``` lp15@70097 ` 652` ``` by (metis (mono_tags)) ``` lp15@70097 ` 653` ``` qed ``` lp15@70097 ` 654` ``` qed (auto intro: that) ``` lp15@70097 ` 655` ``` have "openin (Euclidean_space(Suc n)) lo" ``` lp15@70097 ` 656` ``` apply (simp add: openin_subopen [of _ lo]) ``` lp15@70097 ` 657` ``` apply (simp add: lo_def, safe) ``` lp15@70097 ` 658` ``` apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less) ``` lp15@70097 ` 659` ``` apply (rule_tac x="{x \ topspace(Euclidean_space(Suc n)). x n < 1} ``` lp15@70097 ` 660` ``` \ (topspace(Euclidean_space(Suc n)) - S)" in exI) ``` lp15@70097 ` 661` ``` using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less) ``` lp15@70097 ` 662` ``` done ``` lp15@70097 ` 663` ``` moreover have "openin (Euclidean_space(Suc n)) hi" ``` lp15@70097 ` 664` ``` apply (simp add: openin_subopen [of _ hi]) ``` lp15@70097 ` 665` ``` apply (simp add: hi_def, safe) ``` lp15@70097 ` 666` ``` apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less) ``` lp15@70097 ` 667` ``` apply (rule_tac x="{x \ topspace(Euclidean_space(Suc n)). x n > -1} ``` lp15@70097 ` 668` ``` \ (topspace(Euclidean_space(Suc n)) - S)" in exI) ``` lp15@70097 ` 669` ``` using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less) ``` lp15@70097 ` 670` ``` done ``` lp15@70097 ` 671` ``` ultimately ``` lp15@70097 ` 672` ``` have *: "subtopology (Euclidean_space (Suc n)) (lo \ hi) closure_of ``` lp15@70097 ` 673` ``` (topspace (subtopology (Euclidean_space (Suc n)) (lo \ hi)) - hi) ``` lp15@70097 ` 674` ``` \ subtopology (Euclidean_space (Suc n)) (lo \ hi) interior_of lo" ``` lp15@70097 ` 675` ``` by (metis (no_types, lifting) Diff_idemp Diff_subset_conv Un_commute Un_upper2 closure_of_interior_of interior_of_closure_of interior_of_complement interior_of_eq lo_hi_Un openin_Un openin_open_subtopology topspace_subtopology_subset) ``` lp15@70097 ` 676` ``` have eq: "((lo \ hi) \ (lo \ hi - (topspace (Euclidean_space (Suc n)) \ (lo \ hi) - hi))) = hi" ``` lp15@70097 ` 677` ``` "(lo - (topspace (Euclidean_space (Suc n)) \ (lo \ hi) - hi)) = lo \ hi" ``` lp15@70097 ` 678` ``` by (auto simp: lo_def hi_def Euclidean_space_def) ``` lp15@70097 ` 679` ``` show ?thesis ``` lp15@70097 ` 680` ``` using homology_excision_axiom [OF *, of "lo \ hi" p] ``` lp15@70097 ` 681` ``` by (force simp: subtopology_subtopology eq is_iso_def) ``` lp15@70097 ` 682` ``` qed ``` lp15@70097 ` 683` ``` also have "\ \ relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo \ hi)) lo" ``` lp15@70097 ` 684` ``` by simp ``` lp15@70097 ` 685` ``` also have "\ \ relative_homology_group (p + 1) (Euclidean_space (Suc n)) (lo \ hi)" ``` lp15@70097 ` 686` ``` proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_relboundary_contractible]) ``` lp15@70097 ` 687` ``` have proj: "continuous_map (powertop_real UNIV) euclideanreal (\f. f n)" ``` lp15@70097 ` 688` ``` by (metis UNIV_I continuous_map_product_projection) ``` lp15@70097 ` 689` ``` have hilo: "\x. x \ hi \ (\i. if i = n then - x i else x i) \ lo" ``` lp15@70097 ` 690` ``` "\x. x \ lo \ (\i. if i = n then - x i else x i) \ hi" ``` lp15@70097 ` 691` ``` using local.cong ``` lp15@70097 ` 692` ``` by (auto simp: hi_def lo_def topspace_Euclidean_space split: if_split_asm) ``` lp15@70097 ` 693` ``` have "subtopology (Euclidean_space (Suc n)) hi homeomorphic_space subtopology (Euclidean_space (Suc n)) lo" ``` lp15@70097 ` 694` ``` unfolding homeomorphic_space_def ``` lp15@70097 ` 695` ``` apply (rule_tac x="\x i. if i = n then -(x i) else x i" in exI)+ ``` lp15@70097 ` 696` ``` using proj ``` lp15@70097 ` 697` ``` apply (auto simp: homeomorphic_maps_def Euclidean_space_def continuous_map_in_subtopology ``` lp15@70097 ` 698` ``` hilo continuous_map_componentwise_UNIV continuous_map_from_subtopology continuous_map_minus ``` lp15@70097 ` 699` ``` intro: continuous_map_from_subtopology continuous_map_product_projection) ``` lp15@70097 ` 700` ``` done ``` lp15@70097 ` 701` ``` then have "contractible_space(subtopology (Euclidean_space(Suc n)) hi) ``` lp15@70097 ` 702` ``` \ contractible_space (subtopology (Euclidean_space (Suc n)) lo)" ``` lp15@70097 ` 703` ``` by (rule homeomorphic_space_contractibility) ``` lp15@70097 ` 704` ``` then show "contractible_space (subtopology (Euclidean_space (Suc n)) lo)" ``` lp15@70097 ` 705` ``` using cs_hi by auto ``` lp15@70097 ` 706` ``` show "topspace (Euclidean_space (Suc n)) \ lo \ {}" ``` lp15@70097 ` 707` ``` apply (simp add: lo_def Euclidean_space_def set_eq_iff) ``` lp15@70097 ` 708` ``` apply (rule_tac x="\i. if i = n then -1 else 0" in exI, auto) ``` lp15@70097 ` 709` ``` done ``` lp15@70097 ` 710` ``` qed auto ``` lp15@70097 ` 711` ``` also have "\ \ ?rhs" ``` lp15@70097 ` 712` ``` by (simp flip: lo_hi_Un) ``` lp15@70097 ` 713` ``` finally show ?thesis . ``` lp15@70097 ` 714` ``` qed ``` lp15@70097 ` 715` ``` show ?thesis ``` lp15@70097 ` 716` ``` proof (induction k) ``` lp15@70097 ` 717` ``` case (Suc m) ``` lp15@70097 ` 718` ``` with assms obtain T where cloT: "closedin (powertop_real UNIV) T" ``` lp15@70097 ` 719` ``` and SeqT: "S = T \ {x. \i\n. x i = 0}" ``` lp15@70097 ` 720` ``` by (auto simp: Euclidean_space_def closedin_subtopology) ``` lp15@70097 ` 721` ``` then have "closedin (Euclidean_space (m + n)) S" ``` lp15@70097 ` 722` ``` apply (simp add: Euclidean_space_def closedin_subtopology) ``` lp15@70097 ` 723` ``` apply (rule_tac x="T \ topspace(Euclidean_space n)" in exI) ``` lp15@70097 ` 724` ``` using closedin_Euclidean_space topspace_Euclidean_space by force ``` lp15@70097 ` 725` ``` moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) ``` lp15@70097 ` 726` ``` \ relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)" ``` lp15@70097 ` 727` ``` if "closedin (Euclidean_space n) S" for p n ``` lp15@70097 ` 728` ``` proof - ``` lp15@70097 ` 729` ``` define S' where "S' \ {x \ topspace(Euclidean_space(Suc n)). (\i. if i < n then x i else 0) \ S}" ``` lp15@70097 ` 730` ``` have Ssub_n: "S \ topspace (Euclidean_space n)" ``` lp15@70097 ` 731` ``` by (meson that closedin_def) ``` lp15@70097 ` 732` ``` have "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S') ``` lp15@70097 ` 733` ``` \ relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \ S'. x n = 0})" ``` lp15@70097 ` 734` ``` proof (rule *) ``` lp15@70097 ` 735` ``` have cm: "continuous_map (powertop_real UNIV) euclideanreal (\f. f u)" for u ``` lp15@70097 ` 736` ``` by (metis UNIV_I continuous_map_product_projection) ``` lp15@70097 ` 737` ``` have "continuous_map (subtopology (powertop_real UNIV) {x. \i>n. x i = 0}) euclideanreal ``` lp15@70097 ` 738` ``` (\x. if k \ n then x k else 0)" for k ``` lp15@70097 ` 739` ``` by (simp add: continuous_map_from_subtopology [OF cm]) ``` lp15@70097 ` 740` ``` moreover have "\i\n. (if i < n then x i else 0) = 0" ``` lp15@70097 ` 741` ``` if "x \ topspace (subtopology (powertop_real UNIV) {x. \i>n. x i = 0})" for x ``` lp15@70097 ` 742` ``` using that by simp ``` lp15@70097 ` 743` ``` ultimately have "continuous_map (Euclidean_space (Suc n)) (Euclidean_space n) (\x i. if i < n then x i else 0)" ``` lp15@70097 ` 744` ``` by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV ``` lp15@70097 ` 745` ``` continuous_map_from_subtopology [OF cm] image_subset_iff) ``` lp15@70097 ` 746` ``` then show "closedin (Euclidean_space (Suc n)) S'" ``` lp15@70097 ` 747` ``` unfolding S'_def using that by (rule closedin_continuous_map_preimage) ``` lp15@70097 ` 748` ``` next ``` lp15@70097 ` 749` ``` fix x y ``` lp15@70097 ` 750` ``` assume xy: "\i. i \ n \ x i = y i" "x \ S'" ``` lp15@70097 ` 751` ``` then have "(\i. if i < n then x i else 0) = (\i. if i < n then y i else 0)" ``` lp15@70097 ` 752` ``` by (simp add: S'_def Euclidean_space_def fun_eq_iff) ``` lp15@70097 ` 753` ``` with xy show "y \ S'" ``` lp15@70097 ` 754` ``` by (simp add: S'_def Euclidean_space_def) ``` lp15@70097 ` 755` ``` qed ``` lp15@70097 ` 756` ``` moreover ``` lp15@70097 ` 757` ``` have abs_eq: "(\i. if i < n then x i else 0) = x" if "\i. i \ n \ x i = 0" for x :: "nat \ real" and n ``` lp15@70097 ` 758` ``` using that by auto ``` lp15@70097 ` 759` ``` then have "topspace (Euclidean_space n) - S' = topspace (Euclidean_space n) - S" ``` lp15@70097 ` 760` ``` by (simp add: S'_def Euclidean_space_def set_eq_iff cong: conj_cong) ``` lp15@70097 ` 761` ``` moreover ``` lp15@70097 ` 762` ``` have "topspace (Euclidean_space (Suc n)) - {x \ S'. x n = 0} = topspace (Euclidean_space (Suc n)) - S" ``` lp15@70097 ` 763` ``` using Ssub_n ``` lp15@70097 ` 764` ``` apply (auto simp: S'_def subset_iff Euclidean_space_def set_eq_iff abs_eq cong: conj_cong) ``` lp15@70097 ` 765` ``` by (metis abs_eq le_antisym not_less_eq_eq) ``` lp15@70097 ` 766` ``` ultimately show ?thesis ``` lp15@70097 ` 767` ``` by simp ``` lp15@70097 ` 768` ``` qed ``` lp15@70097 ` 769` ``` ultimately have "relative_homology_group (p + m)(Euclidean_space (m + n))(topspace (Euclidean_space (m + n)) - S) ``` lp15@70097 ` 770` ``` \ relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)" ``` lp15@70097 ` 771` ``` by (metis \closedin (Euclidean_space (m + n)) S\) ``` lp15@70097 ` 772` ``` then show ?case ``` lp15@70097 ` 773` ``` using Suc.IH iso_trans by (force simp: algebra_simps) ``` lp15@70097 ` 774` ``` qed (simp add: iso_refl) ``` lp15@70097 ` 775` ```qed ``` lp15@70097 ` 776` lp15@70097 ` 777` ```lemma iso_Euclidean_complements_lemma1: ``` lp15@70097 ` 778` ``` assumes S: "closedin (Euclidean_space m) S" and cmf: "continuous_map(subtopology (Euclidean_space m) S) (Euclidean_space n) f" ``` lp15@70097 ` 779` ``` obtains g where "continuous_map (Euclidean_space m) (Euclidean_space n) g" ``` lp15@70097 ` 780` ``` "\x. x \ S \ g x = f x" ``` lp15@70097 ` 781` ```proof - ``` lp15@70097 ` 782` ``` have cont: "continuous_on (topspace (Euclidean_space m) \ S) (\x. f x i)" for i ``` lp15@70097 ` 783` ``` by (metis (no_types) continuous_on_product_then_coordinatewise ``` lp15@70097 ` 784` ``` cm_Euclidean_space_iff_continuous_on cmf topspace_subtopology) ``` lp15@70097 ` 785` ``` have "f ` (topspace (Euclidean_space m) \ S) \ topspace (Euclidean_space n)" ``` lp15@70097 ` 786` ``` using cmf continuous_map_image_subset_topspace by fastforce ``` lp15@70097 ` 787` ``` then ``` lp15@70097 ` 788` ``` have "\g. continuous_on (topspace (Euclidean_space m)) g \ (\x \ S. g x = f x i)" for i ``` lp15@70097 ` 789` ``` using S Tietze_unbounded [OF cont [of i]] ``` lp15@70097 ` 790` ``` by (metis closedin_Euclidean_space_iff closedin_closed_Int topspace_subtopology topspace_subtopology_subset) ``` lp15@70097 ` 791` ``` then obtain g where cmg: "\i. continuous_map (Euclidean_space m) euclideanreal (g i)" ``` lp15@70097 ` 792` ``` and gf: "\i x. x \ S \ g i x = f x i" ``` lp15@70097 ` 793` ``` unfolding continuous_map_Euclidean_space_iff by metis ``` lp15@70097 ` 794` ``` let ?GG = "\x i. if i < n then g i x else 0" ``` lp15@70097 ` 795` ``` show thesis ``` lp15@70097 ` 796` ``` proof ``` lp15@70097 ` 797` ``` show "continuous_map (Euclidean_space m) (Euclidean_space n) ?GG" ``` lp15@70097 ` 798` ``` unfolding Euclidean_space_def [of n] ``` lp15@70097 ` 799` ``` by (auto simp: continuous_map_in_subtopology continuous_map_componentwise cmg) ``` lp15@70097 ` 800` ``` show "?GG x = f x" if "x \ S" for x ``` lp15@70097 ` 801` ``` proof - ``` lp15@70097 ` 802` ``` have "S \ topspace (Euclidean_space m)" ``` lp15@70097 ` 803` ``` by (meson S closedin_def) ``` lp15@70097 ` 804` ``` then have "f x \ topspace (Euclidean_space n)" ``` lp15@70097 ` 805` ``` using cmf that unfolding continuous_map_def topspace_subtopology by blast ``` lp15@70097 ` 806` ``` then show ?thesis ``` lp15@70097 ` 807` ``` by (force simp: topspace_Euclidean_space gf that) ``` lp15@70097 ` 808` ``` qed ``` lp15@70097 ` 809` ``` qed ``` lp15@70097 ` 810` ```qed ``` lp15@70097 ` 811` lp15@70097 ` 812` lp15@70097 ` 813` ```lemma iso_Euclidean_complements_lemma2: ``` lp15@70097 ` 814` ``` assumes S: "closedin (Euclidean_space m) S" ``` lp15@70097 ` 815` ``` and T: "closedin (Euclidean_space n) T" ``` lp15@70097 ` 816` ``` and hom: "homeomorphic_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f" ``` lp15@70097 ` 817` ``` obtains g where "homeomorphic_map (prod_topology (Euclidean_space m) (Euclidean_space n)) ``` lp15@70097 ` 818` ``` (prod_topology (Euclidean_space n) (Euclidean_space m)) g" ``` lp15@70097 ` 819` ``` "\x. x \ S \ g(x,(\i. 0)) = (f x,(\i. 0))" ``` lp15@70097 ` 820` ```proof - ``` lp15@70097 ` 821` ``` obtain g where cmf: "continuous_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f" ``` lp15@70097 ` 822` ``` and cmg: "continuous_map (subtopology (Euclidean_space n) T) (subtopology (Euclidean_space m) S) g" ``` lp15@70097 ` 823` ``` and gf: "\x. x \ S \ g (f x) = x" ``` lp15@70097 ` 824` ``` and fg: "\y. y \ T \ f (g y) = y" ``` lp15@70097 ` 825` ``` using hom S T closedin_subset unfolding homeomorphic_map_maps homeomorphic_maps_def ``` lp15@70097 ` 826` ``` by fastforce ``` lp15@70097 ` 827` ``` obtain f' where cmf': "continuous_map (Euclidean_space m) (Euclidean_space n) f'" ``` lp15@70097 ` 828` ``` and f'f: "\x. x \ S \ f' x = f x" ``` lp15@70097 ` 829` ``` using iso_Euclidean_complements_lemma1 S cmf continuous_map_into_fulltopology by metis ``` lp15@70097 ` 830` ``` obtain g' where cmg': "continuous_map (Euclidean_space n) (Euclidean_space m) g'" ``` lp15@70097 ` 831` ``` and g'g: "\x. x \ T \ g' x = g x" ``` lp15@70097 ` 832` ``` using iso_Euclidean_complements_lemma1 T cmg continuous_map_into_fulltopology by metis ``` lp15@70097 ` 833` ``` define p where "p \ \(x,y). (x,(\i. y i + f' x i))" ``` lp15@70097 ` 834` ``` define p' where "p' \ \(x,y). (x,(\i. y i - f' x i))" ``` lp15@70097 ` 835` ``` define q where "q \ \(x,y). (x,(\i. y i + g' x i))" ``` lp15@70097 ` 836` ``` define q' where "q' \ \(x,y). (x,(\i. y i - g' x i))" ``` lp15@70097 ` 837` ``` have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n)) ``` lp15@70097 ` 838` ``` (prod_topology (Euclidean_space m) (Euclidean_space n)) ``` lp15@70097 ` 839` ``` p p'" ``` lp15@70097 ` 840` ``` "homeomorphic_maps (prod_topology (Euclidean_space n) (Euclidean_space m)) ``` lp15@70097 ` 841` ``` (prod_topology (Euclidean_space n) (Euclidean_space m)) ``` lp15@70097 ` 842` ``` q q'" ``` lp15@70097 ` 843` ``` "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n)) ``` lp15@70097 ` 844` ``` (prod_topology (Euclidean_space n) (Euclidean_space m)) (\(x,y). (y,x)) (\(x,y). (y,x))" ``` lp15@70097 ` 845` ``` apply (simp_all add: p_def p'_def q_def q'_def homeomorphic_maps_def continuous_map_pairwise) ``` lp15@70097 ` 846` ``` apply (force simp: case_prod_unfold continuous_map_of_fst [unfolded o_def] cmf' cmg' intro: continuous_intros)+ ``` lp15@70097 ` 847` ``` done ``` lp15@70097 ` 848` ``` then have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n)) ``` lp15@70097 ` 849` ``` (prod_topology (Euclidean_space n) (Euclidean_space m)) ``` lp15@70097 ` 850` ``` (q' \ (\(x,y). (y,x)) \ p) (p' \ ((\(x,y). (y,x)) \ q))" ``` lp15@70097 ` 851` ``` using homeomorphic_maps_compose homeomorphic_maps_sym by (metis (no_types, lifting)) ``` lp15@70097 ` 852` ``` moreover ``` lp15@70097 ` 853` ``` have "\x. x \ S \ (q' \ (\(x,y). (y,x)) \ p) (x, \i. 0) = (f x, \i. 0)" ``` lp15@70097 ` 854` ``` apply (simp add: q'_def p_def f'f) ``` lp15@70097 ` 855` ``` apply (simp add: fun_eq_iff) ``` lp15@70097 ` 856` ``` by (metis S T closedin_subset g'g gf hom homeomorphic_imp_surjective_map image_eqI topspace_subtopology_subset) ``` lp15@70097 ` 857` ``` ultimately ``` lp15@70097 ` 858` ``` show thesis ``` lp15@70097 ` 859` ``` using homeomorphic_map_maps that by blast ``` lp15@70097 ` 860` ```qed ``` lp15@70097 ` 861` lp15@70097 ` 862` lp15@70097 ` 863` ```proposition isomorphic_relative_homology_groups_Euclidean_complements: ``` lp15@70097 ` 864` ``` assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T" ``` lp15@70097 ` 865` ``` and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 866` ``` shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S) ``` lp15@70097 ` 867` ``` \ relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)" ``` lp15@70097 ` 868` ```proof - ``` lp15@70097 ` 869` ``` have subST: "S \ topspace(Euclidean_space n)" "T \ topspace(Euclidean_space n)" ``` lp15@70097 ` 870` ``` by (meson S T closedin_def)+ ``` lp15@70097 ` 871` ``` have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) ``` lp15@70097 ` 872` ``` \ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)" ``` lp15@70097 ` 873` ``` using relative_homology_group_Euclidean_complement_step [OF S] by blast ``` lp15@70097 ` 874` ``` moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T) ``` lp15@70097 ` 875` ``` \ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)" ``` lp15@70097 ` 876` ``` using relative_homology_group_Euclidean_complement_step [OF T] by blast ``` lp15@70097 ` 877` ``` moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S) ``` lp15@70097 ` 878` ``` \ relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)" ``` lp15@70097 ` 879` ``` proof - ``` lp15@70097 ` 880` ``` obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S) ``` lp15@70097 ` 881` ``` (subtopology (Euclidean_space n) T) f" ``` lp15@70097 ` 882` ``` using hom unfolding homeomorphic_space by blast ``` lp15@70097 ` 883` ``` obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n)) ``` lp15@70097 ` 884` ``` (prod_topology (Euclidean_space n) (Euclidean_space n)) g" ``` lp15@70097 ` 885` ``` and gf: "\x. x \ S \ g(x,(\i. 0)) = (f x,(\i. 0))" ``` lp15@70097 ` 886` ``` using S T f iso_Euclidean_complements_lemma2 by blast ``` lp15@70097 ` 887` ``` define h where "h \ \x::nat \real. ((\i. if i < n then x i else 0), (\j. if j < n then x(n + j) else 0))" ``` lp15@70097 ` 888` ``` define k where "k \ \(x,y) i. if i < 2 * n then if i < n then x i else y(i - n) else (0::real)" ``` lp15@70097 ` 889` ``` have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k" ``` lp15@70097 ` 890` ``` unfolding homeomorphic_maps_def ``` lp15@70097 ` 891` ``` proof safe ``` lp15@70097 ` 892` ``` show "continuous_map (Euclidean_space (2 * n)) ``` lp15@70097 ` 893` ``` (prod_topology (Euclidean_space n) (Euclidean_space n)) h" ``` lp15@70097 ` 894` ``` apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space) ``` lp15@70097 ` 895` ``` unfolding Euclidean_space_def ``` lp15@70097 ` 896` ``` by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection) ``` lp15@70097 ` 897` ``` have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\p. fst p i)" for i ``` lp15@70097 ` 898` ``` using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce ``` lp15@70097 ` 899` ``` moreover ``` lp15@70097 ` 900` ``` have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\p. snd p (i - n))" for i ``` lp15@70097 ` 901` ``` using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce ``` lp15@70097 ` 902` ``` ultimately ``` lp15@70097 ` 903` ``` show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) ``` lp15@70097 ` 904` ``` (Euclidean_space (2 * n)) k" ``` lp15@70097 ` 905` ``` by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold) ``` lp15@70097 ` 906` ``` qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space) ``` lp15@70097 ` 907` ``` define kgh where "kgh \ k \ g \ h" ``` lp15@70097 ` 908` ``` let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S) ``` lp15@70097 ` 909` ``` (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh" ``` lp15@70097 ` 910` ``` have "?i \ iso (relative_homology_group (p + int n) (Euclidean_space (2 * n)) ``` lp15@70097 ` 911` ``` (topspace (Euclidean_space (2 * n)) - S)) ``` lp15@70097 ` 912` ``` (relative_homology_group (p + int n) (Euclidean_space (2 * n)) ``` lp15@70097 ` 913` ``` (topspace (Euclidean_space (2 * n)) - T))" ``` lp15@70097 ` 914` ``` proof (rule homeomorphic_map_relative_homology_iso) ``` lp15@70097 ` 915` ``` show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh" ``` lp15@70097 ` 916` ``` unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym) ``` lp15@70097 ` 917` ``` have Teq: "T = f ` S" ``` lp15@70097 ` 918` ``` using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast ``` lp15@70097 ` 919` ``` have khf: "\x. x \ S \ k(h(f x)) = f x" ``` lp15@70097 ` 920` ``` by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space) ``` lp15@70097 ` 921` ``` have gh: "g(h x) = h(f x)" if "x \ S" for x ``` lp15@70097 ` 922` ``` proof - ``` lp15@70097 ` 923` ``` have [simp]: "(\i. if i < n then x i else 0) = x" ``` lp15@70097 ` 924` ``` using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff) ``` lp15@70097 ` 925` ``` have "f x \ topspace(Euclidean_space n)" ``` lp15@70097 ` 926` ``` using Teq subST(2) that by blast ``` lp15@70097 ` 927` ``` moreover have "(\j. if j < n then x (n + j) else 0) = (\j. 0::real)" ``` lp15@70097 ` 928` ``` using Euclidean_space_def subST(1) that by force ``` lp15@70097 ` 929` ``` ultimately show ?thesis ``` lp15@70097 ` 930` ``` by (simp add: topspace_Euclidean_space h_def gf \x \ S\ fun_eq_iff) ``` lp15@70097 ` 931` ``` qed ``` lp15@70097 ` 932` ``` have *: "\S \ U; T \ U; kgh ` U = U; inj_on kgh U; kgh ` S = T\ \ kgh ` (U - S) = U - T" for U ``` lp15@70097 ` 933` ``` unfolding inj_on_def set_eq_iff by blast ``` lp15@70097 ` 934` ``` show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T" ``` lp15@70097 ` 935` ``` proof (rule *) ``` lp15@70097 ` 936` ``` show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))" ``` lp15@70097 ` 937` ``` by (simp add: hm homeomorphic_imp_surjective_map) ``` lp15@70097 ` 938` ``` show "inj_on kgh (topspace (Euclidean_space (2 * n)))" ``` lp15@70097 ` 939` ``` using hm homeomorphic_map_def by auto ``` lp15@70097 ` 940` ``` show "kgh ` S = T" ``` lp15@70097 ` 941` ``` by (simp add: Teq kgh_def gh khf) ``` lp15@70097 ` 942` ``` qed (use subST topspace_Euclidean_space in \fastforce+\) ``` lp15@70097 ` 943` ``` qed auto ``` lp15@70097 ` 944` ``` then show ?thesis ``` lp15@70097 ` 945` ``` by (simp add: is_isoI mult_2) ``` lp15@70097 ` 946` ``` qed ``` lp15@70097 ` 947` ``` ultimately show ?thesis ``` lp15@70097 ` 948` ``` by (meson group.iso_sym iso_trans group_relative_homology_group) ``` lp15@70097 ` 949` ```qed ``` lp15@70097 ` 950` lp15@70097 ` 951` ```lemma lemma_iod: ``` lp15@70097 ` 952` ``` assumes "S \ T" "S \ {}" and Tsub: "T \ topspace(Euclidean_space n)" ``` lp15@70097 ` 953` ``` and S: "\a b u. \a \ S; b \ T; 0 < u; u < 1\ \ (\i. (1 - u) * a i + u * b i) \ S" ``` lp15@70097 ` 954` ``` shows "path_connectedin (Euclidean_space n) T" ``` lp15@70097 ` 955` ```proof - ``` lp15@70097 ` 956` ``` obtain a where "a \ S" ``` lp15@70097 ` 957` ``` using assms by blast ``` lp15@70097 ` 958` ``` have "path_component_of (subtopology (Euclidean_space n) T) a b" if "b \ T" for b ``` lp15@70097 ` 959` ``` unfolding path_component_of_def ``` lp15@70097 ` 960` ``` proof (intro exI conjI) ``` lp15@70097 ` 961` ``` have [simp]: "\i\n. a i = 0" ``` lp15@70097 ` 962` ``` using Tsub \a \ S\ assms(1) topspace_Euclidean_space by auto ``` lp15@70097 ` 963` ``` have [simp]: "\i\n. b i = 0" ``` lp15@70097 ` 964` ``` using Tsub that topspace_Euclidean_space by auto ``` lp15@70097 ` 965` ``` have inT: "(\i. (1 - x) * a i + x * b i) \ T" if "0 \ x" "x \ 1" for x ``` lp15@70097 ` 966` ``` proof (cases "x = 0 \ x = 1") ``` lp15@70097 ` 967` ``` case True ``` lp15@70097 ` 968` ``` with \a \ S\ \b \ T\ \S \ T\ show ?thesis ``` lp15@70097 ` 969` ``` by force ``` lp15@70097 ` 970` ``` next ``` lp15@70097 ` 971` ``` case False ``` lp15@70097 ` 972` ``` then show ?thesis ``` lp15@70097 ` 973` ``` using subsetD [OF \S \ T\ S] \a \ S\ \b \ T\ that by auto ``` lp15@70097 ` 974` ``` qed ``` lp15@70097 ` 975` ``` have "continuous_on {0..1} (\x. (1 - x) * a k + x * b k)" for k ``` lp15@70097 ` 976` ``` by (intro continuous_intros) ``` lp15@70097 ` 977` ``` then show "pathin (subtopology (Euclidean_space n) T) (\t i. (1 - t) * a i + t * b i)" ``` lp15@70097 ` 978` ``` apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology) ``` lp15@70097 ` 979` ``` apply (simp add: pathin_def continuous_map_componentwise_UNIV inT) ``` lp15@70097 ` 980` ``` done ``` lp15@70097 ` 981` ``` qed auto ``` lp15@70097 ` 982` ``` then have "path_connected_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 983` ``` by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset) ``` lp15@70097 ` 984` ``` then show ?thesis ``` lp15@70097 ` 985` ``` by (simp add: Tsub path_connectedin_def) ``` lp15@70097 ` 986` ```qed ``` lp15@70097 ` 987` lp15@70097 ` 988` lp15@70097 ` 989` ```lemma invariance_of_dimension_closedin_Euclidean_space: ``` lp15@70097 ` 990` ``` assumes "closedin (Euclidean_space n) S" ``` lp15@70097 ` 991` ``` shows "subtopology (Euclidean_space n) S homeomorphic_space Euclidean_space n ``` lp15@70097 ` 992` ``` \ S = topspace(Euclidean_space n)" ``` lp15@70097 ` 993` ``` (is "?lhs = ?rhs") ``` lp15@70097 ` 994` ```proof ``` lp15@70097 ` 995` ``` assume L: ?lhs ``` lp15@70097 ` 996` ``` have Ssub: "S \ topspace (Euclidean_space n)" ``` lp15@70097 ` 997` ``` by (meson assms closedin_def) ``` lp15@70097 ` 998` ``` moreover have False if "a \ S" and "a \ topspace (Euclidean_space n)" for a ``` lp15@70097 ` 999` ``` proof - ``` lp15@70097 ` 1000` ``` have cl_n: "closedin (Euclidean_space (Suc n)) (topspace(Euclidean_space n))" ``` lp15@70097 ` 1001` ``` using Euclidean_space_def closedin_Euclidean_space closedin_subtopology by fastforce ``` lp15@70097 ` 1002` ``` then have sub: "subtopology (Euclidean_space(Suc n)) (topspace(Euclidean_space n)) = Euclidean_space n" ``` lp15@70097 ` 1003` ``` by (metis (no_types, lifting) Euclidean_space_def closedin_subset subtopology_subtopology topspace_Euclidean_space topspace_subtopology topspace_subtopology_subset) ``` lp15@70097 ` 1004` ``` then have cl_S: "closedin (Euclidean_space(Suc n)) S" ``` lp15@70097 ` 1005` ``` using cl_n assms closedin_closed_subtopology by fastforce ``` lp15@70097 ` 1006` ``` have sub_SucS: "subtopology (Euclidean_space (Suc n)) S = subtopology (Euclidean_space n) S" ``` lp15@70097 ` 1007` ``` by (metis Ssub sub subtopology_subtopology topspace_subtopology topspace_subtopology_subset) ``` lp15@70097 ` 1008` ``` have non0: "{y. \x::nat\real. (\i\Suc n. x i = 0) \ (\i\n. x i \ 0) \ y = x n} = -{0}" ``` lp15@70097 ` 1009` ``` proof safe ``` lp15@70097 ` 1010` ``` show "False" if "\i\Suc n. f i = 0" "0 = f n" "n \ i" "f i \ 0" for f::"nat\real" and i ``` lp15@70097 ` 1011` ``` by (metis that le_antisym not_less_eq_eq) ``` lp15@70097 ` 1012` ``` show "\f::nat\real. (\i\Suc n. f i = 0) \ (\i\n. f i \ 0) \ a = f n" if "a \ 0" for a ``` lp15@70097 ` 1013` ``` by (rule_tac x="(\i. 0)(n:= a)" in exI) (force simp: that) ``` lp15@70097 ` 1014` ``` qed ``` lp15@70097 ` 1015` ``` have "homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)) ``` lp15@70097 ` 1016` ``` \ homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))" ``` lp15@70097 ` 1017` ``` proof (rule isomorphic_relative_contractible_space_imp_homology_groups) ``` lp15@70097 ` 1018` ``` show "(topspace (Euclidean_space (Suc n)) - S = {}) = ``` lp15@70097 ` 1019` ``` (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n) = {})" ``` lp15@70097 ` 1020` ``` using cl_n closedin_subset that by auto ``` lp15@70097 ` 1021` ``` next ``` lp15@70097 ` 1022` ``` fix p ``` lp15@70097 ` 1023` ``` show "relative_homology_group p (Euclidean_space (Suc n)) ``` lp15@70097 ` 1024` ``` (topspace (Euclidean_space (Suc n)) - S) \ ``` lp15@70097 ` 1025` ``` relative_homology_group p (Euclidean_space (Suc n)) ``` lp15@70097 ` 1026` ``` (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n))" ``` lp15@70097 ` 1027` ``` by (simp add: L sub_SucS cl_S cl_n isomorphic_relative_homology_groups_Euclidean_complements sub) ``` lp15@70097 ` 1028` ``` qed (auto simp: L) ``` lp15@70097 ` 1029` ``` moreover ``` lp15@70097 ` 1030` ``` have "continuous_map (powertop_real UNIV) euclideanreal (\x. x n)" ``` lp15@70097 ` 1031` ``` by (metis (no_types) UNIV_I continuous_map_product_projection) ``` lp15@70097 ` 1032` ``` then have cm: "continuous_map (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n))) ``` lp15@70097 ` 1033` ``` euclideanreal (\x. x n)" ``` lp15@70097 ` 1034` ``` by (simp add: Euclidean_space_def continuous_map_from_subtopology) ``` lp15@70097 ` 1035` ``` have False if "path_connected_space ``` lp15@70097 ` 1036` ``` (subtopology (Euclidean_space (Suc n)) ``` lp15@70097 ` 1037` ``` (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))" ``` lp15@70097 ` 1038` ``` using path_connectedin_continuous_map_image [OF cm that [unfolded path_connectedin_topspace [symmetric]]] ``` lp15@70097 ` 1039` ``` bounded_path_connected_Compl_real [of "{0}"] ``` lp15@70097 ` 1040` ``` by (simp add: topspace_Euclidean_space image_def Bex_def non0 flip: path_connectedin_topspace) ``` lp15@70097 ` 1041` ``` moreover ``` lp15@70097 ` 1042` ``` have eq: "T = T \ {x. x n \ 0} \ T \ {x. x n \ 0}" for T :: "(nat \ real) set" ``` lp15@70097 ` 1043` ``` by auto ``` lp15@70097 ` 1044` ``` have "path_connectedin (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)" ``` lp15@70097 ` 1045` ``` proof (subst eq, rule path_connectedin_Un) ``` lp15@70097 ` 1046` ``` have "topspace(Euclidean_space(Suc n)) \ {x. x n = 0} = topspace(Euclidean_space n)" ``` lp15@70097 ` 1047` ``` apply (auto simp: topspace_Euclidean_space) ``` lp15@70097 ` 1048` ``` by (metis Suc_leI inf.absorb_iff2 inf.orderE leI) ``` lp15@70097 ` 1049` ``` let ?S = "topspace(Euclidean_space(Suc n)) \ {x. x n < 0}" ``` lp15@70097 ` 1050` ``` show "path_connectedin (Euclidean_space (Suc n)) ``` lp15@70097 ` 1051` ``` ((topspace (Euclidean_space (Suc n)) - S) \ {x. x n \ 0})" ``` lp15@70097 ` 1052` ``` proof (rule lemma_iod) ``` lp15@70097 ` 1053` ``` show "?S \ (topspace (Euclidean_space (Suc n)) - S) \ {x. x n \ 0}" ``` lp15@70097 ` 1054` ``` using Ssub topspace_Euclidean_space by auto ``` lp15@70097 ` 1055` ``` show "?S \ {}" ``` lp15@70097 ` 1056` ``` apply (simp add: topspace_Euclidean_space set_eq_iff) ``` lp15@70097 ` 1057` ``` apply (rule_tac x="(\i. 0)(n:= -1)" in exI) ``` lp15@70097 ` 1058` ``` apply auto ``` lp15@70097 ` 1059` ``` done ``` lp15@70097 ` 1060` ``` fix a b and u::real ``` lp15@70097 ` 1061` ``` assume ``` lp15@70097 ` 1062` ``` "a \ ?S" "0 < u" "u < 1" ``` lp15@70097 ` 1063` ``` "b \ (topspace (Euclidean_space (Suc n)) - S) \ {x. x n \ 0}" ``` lp15@70097 ` 1064` ``` then show "(\i. (1 - u) * a i + u * b i) \ ?S" ``` lp15@70097 ` 1065` ``` by (simp add: topspace_Euclidean_space add_neg_nonpos less_eq_real_def mult_less_0_iff) ``` lp15@70097 ` 1066` ``` qed (simp add: topspace_Euclidean_space subset_iff) ``` lp15@70097 ` 1067` ``` let ?T = "topspace(Euclidean_space(Suc n)) \ {x. x n > 0}" ``` lp15@70097 ` 1068` ``` show "path_connectedin (Euclidean_space (Suc n)) ``` lp15@70097 ` 1069` ``` ((topspace (Euclidean_space (Suc n)) - S) \ {x. 0 \ x n})" ``` lp15@70097 ` 1070` ``` proof (rule lemma_iod) ``` lp15@70097 ` 1071` ``` show "?T \ (topspace (Euclidean_space (Suc n)) - S) \ {x. 0 \ x n}" ``` lp15@70097 ` 1072` ``` using Ssub topspace_Euclidean_space by auto ``` lp15@70097 ` 1073` ``` show "?T \ {}" ``` lp15@70097 ` 1074` ``` apply (simp add: topspace_Euclidean_space set_eq_iff) ``` lp15@70097 ` 1075` ``` apply (rule_tac x="(\i. 0)(n:= 1)" in exI) ``` lp15@70097 ` 1076` ``` apply auto ``` lp15@70097 ` 1077` ``` done ``` lp15@70097 ` 1078` ``` fix a b and u::real ``` lp15@70097 ` 1079` ``` assume "a \ ?T" "0 < u" "u < 1" "b \ (topspace (Euclidean_space (Suc n)) - S) \ {x. 0 \ x n}" ``` lp15@70097 ` 1080` ``` then show "(\i. (1 - u) * a i + u * b i) \ ?T" ``` lp15@70097 ` 1081` ``` by (simp add: topspace_Euclidean_space add_pos_nonneg) ``` lp15@70097 ` 1082` ``` qed (simp add: topspace_Euclidean_space subset_iff) ``` lp15@70097 ` 1083` ``` show "(topspace (Euclidean_space (Suc n)) - S) \ {x. x n \ 0} \ ``` lp15@70097 ` 1084` ``` ((topspace (Euclidean_space (Suc n)) - S) \ {x. 0 \ x n}) \ {}" ``` lp15@70097 ` 1085` ``` using that ``` lp15@70097 ` 1086` ``` apply (auto simp: Set.set_eq_iff topspace_Euclidean_space) ``` lp15@70097 ` 1087` ``` by (metis Suc_leD order_refl) ``` lp15@70097 ` 1088` ``` qed ``` lp15@70097 ` 1089` ``` then have "path_connected_space (subtopology (Euclidean_space (Suc n)) ``` lp15@70097 ` 1090` ``` (topspace (Euclidean_space (Suc n)) - S))" ``` lp15@70097 ` 1091` ``` apply (simp add: path_connectedin_subtopology flip: path_connectedin_topspace) ``` lp15@70097 ` 1092` ``` by (metis Int_Diff inf_idem) ``` lp15@70097 ` 1093` ``` ultimately ``` lp15@70097 ` 1094` ``` show ?thesis ``` lp15@70097 ` 1095` ``` using isomorphic_homology_imp_path_connectedness by blast ``` lp15@70097 ` 1096` ``` qed ``` lp15@70097 ` 1097` ``` ultimately show ?rhs ``` lp15@70097 ` 1098` ``` by blast ``` lp15@70097 ` 1099` ```qed (simp add: homeomorphic_space_refl) ``` lp15@70097 ` 1100` lp15@70097 ` 1101` lp15@70097 ` 1102` lp15@70097 ` 1103` ```lemma isomorphic_homology_groups_Euclidean_complements: ``` lp15@70097 ` 1104` ``` assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T" ``` lp15@70097 ` 1105` ``` "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 1106` ``` shows "homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - S)) ``` lp15@70097 ` 1107` ``` \ homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - T))" ``` lp15@70097 ` 1108` ```proof (rule isomorphic_relative_contractible_space_imp_homology_groups) ``` lp15@70097 ` 1109` ``` show "topspace (Euclidean_space n) - S \ topspace (Euclidean_space n)" ``` lp15@70097 ` 1110` ``` using assms homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subtopology_superset by fastforce ``` lp15@70097 ` 1111` ``` show "topspace (Euclidean_space n) - T \ topspace (Euclidean_space n)" ``` lp15@70097 ` 1112` ``` using assms invariance_of_dimension_closedin_Euclidean_space subtopology_superset by force ``` lp15@70097 ` 1113` ``` show "(topspace (Euclidean_space n) - S = {}) = (topspace (Euclidean_space n) - T = {})" ``` lp15@70097 ` 1114` ``` by (metis Diff_eq_empty_iff assms closedin_subset homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_antisym subtopology_topspace) ``` lp15@70097 ` 1115` ``` show "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) \ ``` lp15@70097 ` 1116` ``` relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)" for p ``` lp15@70097 ` 1117` ``` using assms isomorphic_relative_homology_groups_Euclidean_complements by blast ``` lp15@70097 ` 1118` ```qed auto ``` lp15@70097 ` 1119` lp15@70097 ` 1120` ```lemma eqpoll_path_components_Euclidean_complements: ``` lp15@70097 ` 1121` ``` assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T" ``` lp15@70097 ` 1122` ``` "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 1123` ``` shows "path_components_of ``` lp15@70097 ` 1124` ``` (subtopology (Euclidean_space n) ``` lp15@70097 ` 1125` ``` (topspace(Euclidean_space n) - S)) ``` lp15@70097 ` 1126` ``` \ path_components_of ``` lp15@70097 ` 1127` ``` (subtopology (Euclidean_space n) ``` lp15@70097 ` 1128` ``` (topspace(Euclidean_space n) - T))" ``` lp15@70097 ` 1129` ``` by (simp add: assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_components) ``` lp15@70097 ` 1130` lp15@70097 ` 1131` ```lemma path_connectedin_Euclidean_complements: ``` lp15@70097 ` 1132` ``` assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T" ``` lp15@70097 ` 1133` ``` "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 1134` ``` shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S) ``` lp15@70097 ` 1135` ``` \ path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)" ``` lp15@70097 ` 1136` ``` by (meson Diff_subset assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_connectedness path_connectedin_def) ``` lp15@70097 ` 1137` lp15@70097 ` 1138` ```lemma eqpoll_connected_components_Euclidean_complements: ``` lp15@70097 ` 1139` ``` assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T" ``` lp15@70097 ` 1140` ``` and ST: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 1141` ``` shows "connected_components_of ``` lp15@70097 ` 1142` ``` (subtopology (Euclidean_space n) ``` lp15@70097 ` 1143` ``` (topspace(Euclidean_space n) - S)) ``` lp15@70097 ` 1144` ``` \ connected_components_of ``` lp15@70097 ` 1145` ``` (subtopology (Euclidean_space n) ``` lp15@70097 ` 1146` ``` (topspace(Euclidean_space n) - T))" ``` lp15@70097 ` 1147` ``` using eqpoll_path_components_Euclidean_complements [OF assms] ``` lp15@70097 ` 1148` ``` by (metis S T closedin_def locally_path_connected_Euclidean_space locally_path_connected_space_open_subset path_components_eq_connected_components_of) ``` lp15@70097 ` 1149` lp15@70097 ` 1150` ```lemma connected_in_Euclidean_complements: ``` lp15@70097 ` 1151` ``` assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T" ``` lp15@70097 ` 1152` ``` "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)" ``` lp15@70097 ` 1153` ``` shows "connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S) ``` lp15@70097 ` 1154` ``` \ connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)" ``` lp15@70097 ` 1155` ``` apply (simp add: connectedin_def connected_space_iff_components_subset_singleton subset_singleton_iff_lepoll) ``` lp15@70097 ` 1156` ``` using eqpoll_connected_components_Euclidean_complements [OF assms] ``` lp15@70097 ` 1157` ``` by (meson eqpoll_sym lepoll_trans1) ``` lp15@70097 ` 1158` lp15@70097 ` 1159` lp15@70097 ` 1160` ```theorem invariance_of_dimension_Euclidean_space: ``` lp15@70097 ` 1161` ``` "Euclidean_space m homeomorphic_space Euclidean_space n \ m = n" ``` lp15@70097 ` 1162` ```proof (cases m n rule: linorder_cases) ``` lp15@70097 ` 1163` ``` case less ``` lp15@70097 ` 1164` ``` then have *: "topspace (Euclidean_space m) \ topspace (Euclidean_space n)" ``` lp15@70097 ` 1165` ``` by (meson le_cases not_le subset_Euclidean_space) ``` lp15@70097 ` 1166` ``` then have "Euclidean_space m = subtopology (Euclidean_space n) (topspace(Euclidean_space m))" ``` lp15@70097 ` 1167` ``` by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology) ``` lp15@70097 ` 1168` ``` then show ?thesis ``` lp15@70097 ` 1169` ``` by (metis (no_types, lifting) * Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space) ``` lp15@70097 ` 1170` ```next ``` lp15@70097 ` 1171` ``` case equal ``` lp15@70097 ` 1172` ``` then show ?thesis ``` lp15@70097 ` 1173` ``` by (simp add: homeomorphic_space_refl) ``` lp15@70097 ` 1174` ```next ``` lp15@70097 ` 1175` ``` case greater ``` lp15@70097 ` 1176` ``` then have *: "topspace (Euclidean_space n) \ topspace (Euclidean_space m)" ``` lp15@70097 ` 1177` ``` by (meson le_cases not_le subset_Euclidean_space) ``` lp15@70097 ` 1178` ``` then have "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))" ``` lp15@70097 ` 1179` ``` by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology) ``` lp15@70097 ` 1180` ``` then show ?thesis ``` lp15@70097 ` 1181` ``` by (metis (no_types, lifting) "*" Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space) ``` lp15@70097 ` 1182` ```qed ``` lp15@70097 ` 1183` lp15@70097 ` 1184` lp15@70097 ` 1185` lp15@70097 ` 1186` ```lemma biglemma: ``` lp15@70097 ` 1187` ``` assumes "n \ 0" and S: "compactin (Euclidean_space n) S" ``` lp15@70097 ` 1188` ``` and cmh: "continuous_map (subtopology (Euclidean_space n) S) (Euclidean_space n) h" ``` lp15@70097 ` 1189` ``` and "inj_on h S" ``` lp15@70097 ` 1190` ``` shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - h ` S) ``` lp15@70097 ` 1191` ``` \ path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)" ``` lp15@70097 ` 1192` ```proof (rule path_connectedin_Euclidean_complements) ``` lp15@70097 ` 1193` ``` have hS_sub: "h ` S \ topspace(Euclidean_space n)" ``` lp15@70097 ` 1194` ``` by (metis (no_types) S cmh compactin_subspace continuous_map_image_subset_topspace topspace_subtopology_subset) ``` lp15@70097 ` 1195` ``` show clo_S: "closedin (Euclidean_space n) S" ``` lp15@70097 ` 1196` ``` using assms by (simp add: continuous_map_in_subtopology Hausdorff_Euclidean_space compactin_imp_closedin) ``` lp15@70097 ` 1197` ``` show clo_hS: "closedin (Euclidean_space n) (h ` S)" ``` lp15@70097 ` 1198` ``` using Hausdorff_Euclidean_space S cmh compactin_absolute compactin_imp_closedin image_compactin by blast ``` lp15@70097 ` 1199` ``` have "homeomorphic_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h" ``` lp15@70097 ` 1200` ``` proof (rule continuous_imp_homeomorphic_map) ``` lp15@70097 ` 1201` ``` show "compact_space (subtopology (Euclidean_space n) S)" ``` lp15@70097 ` 1202` ``` by (simp add: S compact_space_subtopology) ``` lp15@70097 ` 1203` ``` show "Hausdorff_space (subtopology (Euclidean_space n) (h ` S))" ``` lp15@70097 ` 1204` ``` using hS_sub ``` lp15@70097 ` 1205` ``` by (simp add: Hausdorff_Euclidean_space Hausdorff_space_subtopology) ``` lp15@70097 ` 1206` ``` show "continuous_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h" ``` lp15@70097 ` 1207` ``` using cmh continuous_map_in_subtopology by fastforce ``` lp15@70097 ` 1208` ``` show "h ` topspace (subtopology (Euclidean_space n) S) = topspace (subtopology (Euclidean_space n) (h ` S))" ``` lp15@70097 ` 1209` ``` using clo_hS clo_S closedin_subset by auto ``` lp15@70097 ` 1210` ``` show "inj_on h (topspace (subtopology (Euclidean_space n) S))" ``` lp15@70097 ` 1211` ``` by (metis \inj_on h S\ clo_S closedin_def topspace_subtopology_subset) ``` lp15@70097 ` 1212` ``` qed ``` lp15@70097 ` 1213` ``` then show "subtopology (Euclidean_space n) (h ` S) homeomorphic_space subtopology (Euclidean_space n) S" ``` lp15@70097 ` 1214` ``` using homeomorphic_space homeomorphic_space_sym by blast ``` lp15@70097 ` 1215` ```qed ``` lp15@70097 ` 1216` lp15@70097 ` 1217` lp15@70097 ` 1218` ```lemma lemmaIOD: ``` lp15@70097 ` 1219` ``` assumes ``` lp15@70097 ` 1220` ``` "\T. T \ U \ c \ T" "\T. T \ U \ d \ T" "\U = c \ d" "\T. T \ U \ T \ {}" ``` lp15@70097 ` 1221` ``` "pairwise disjnt U" "~(\T. U \ {T})" ``` lp15@70097 ` 1222` ``` shows "c \ U" ``` lp15@70097 ` 1223` ``` using assms ``` lp15@70097 ` 1224` ``` apply safe ``` lp15@70097 ` 1225` ``` subgoal for C' D' ``` lp15@70097 ` 1226` ``` proof (cases "C'=D'") ``` lp15@70097 ` 1227` ``` show "c \ U" ``` lp15@70097 ` 1228` ``` if UU: "\ U = c \ d" ``` lp15@70097 ` 1229` ``` and U: "\T. T \ U \ T \ {}" "disjoint U" and "\T. U \ {T}" "c \ C'" "D' \ U" "d \ D'" "C' = D'" ``` lp15@70097 ` 1230` ``` proof - ``` lp15@70097 ` 1231` ``` have "c \ d = D'" ``` lp15@70097 ` 1232` ``` using Union_upper sup_mono UU that(5) that(6) that(7) that(8) by auto ``` lp15@70097 ` 1233` ``` then have "\U = D'" ``` lp15@70097 ` 1234` ``` by (simp add: UU) ``` lp15@70097 ` 1235` ``` with U have "U = {D'}" ``` lp15@70097 ` 1236` ``` by (metis (no_types, lifting) disjnt_Union1 disjnt_self_iff_empty insertCI pairwiseD subset_iff that(4) that(6)) ``` lp15@70097 ` 1237` ``` then show ?thesis ``` lp15@70097 ` 1238` ``` using that(4) by auto ``` lp15@70097 ` 1239` ``` qed ``` lp15@70097 ` 1240` ``` show "c \ U" ``` lp15@70097 ` 1241` ``` if "\ U = c \ d""disjoint U" "C' \ U" "c \ C'""D' \ U" "d \ D'" "C' \ D'" ``` lp15@70097 ` 1242` ``` proof - ``` lp15@70097 ` 1243` ``` have "C' \ D' = {}" ``` lp15@70097 ` 1244` ``` using \disjoint U\ \C' \ U\ \D' \ U\ \C' \ D'\unfolding disjnt_iff pairwise_def ``` lp15@70097 ` 1245` ``` by blast ``` lp15@70097 ` 1246` ``` then show ?thesis ``` lp15@70097 ` 1247` ``` using subset_antisym that(1) \C' \ U\ \c \ C'\ \d \ D'\ by fastforce ``` lp15@70097 ` 1248` ``` qed ``` lp15@70097 ` 1249` ``` qed ``` lp15@70097 ` 1250` ``` done ``` lp15@70097 ` 1251` lp15@70097 ` 1252` lp15@70097 ` 1253` lp15@70097 ` 1254` lp15@70097 ` 1255` ```theorem invariance_of_domain_Euclidean_space: ``` lp15@70097 ` 1256` ``` assumes U: "openin (Euclidean_space n) U" ``` lp15@70097 ` 1257` ``` and cmf: "continuous_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f" ``` lp15@70097 ` 1258` ``` and "inj_on f U" ``` lp15@70097 ` 1259` ``` shows "openin (Euclidean_space n) (f ` U)" (is "openin ?E (f ` U)") ``` lp15@70097 ` 1260` ```proof (cases "n = 0") ``` lp15@70097 ` 1261` ``` case True ``` lp15@70097 ` 1262` ``` have [simp]: "Euclidean_space 0 = discrete_topology {\i. 0}" ``` lp15@70097 ` 1263` ``` by (auto simp: subtopology_eq_discrete_topology_sing topspace_Euclidean_space) ``` lp15@70097 ` 1264` ``` show ?thesis ``` lp15@70097 ` 1265` ``` using cmf True U by auto ``` lp15@70097 ` 1266` ```next ``` lp15@70097 ` 1267` ``` case False ``` lp15@70097 ` 1268` ``` define enorm where "enorm \ \x. sqrt(\ii. if i = k then d else 0) = (if k < n then \d\ else 0)" for k d ``` lp15@70097 ` 1270` ``` using \n \ 0\ by (auto simp: enorm_def power2_eq_square if_distrib [of "\x. x * _"] cong: if_cong) ``` lp15@70097 ` 1271` ``` define zero::"nat\real" where "zero \ \i. 0" ``` lp15@70097 ` 1272` ``` have zero_in [simp]: "zero \ topspace ?E" ``` lp15@70097 ` 1273` ``` using False by (simp add: zero_def topspace_Euclidean_space) ``` lp15@70097 ` 1274` ``` have enorm_eq_0 [simp]: "enorm x = 0 \ x = zero" ``` lp15@70097 ` 1275` ``` if "x \ topspace(Euclidean_space n)" for x ``` lp15@70097 ` 1276` ``` using that unfolding zero_def enorm_def ``` lp15@70097 ` 1277` ``` apply (simp add: sum_nonneg_eq_0_iff fun_eq_iff topspace_Euclidean_space) ``` lp15@70097 ` 1278` ``` using le_less_linear by blast ``` lp15@70097 ` 1279` ``` have [simp]: "enorm zero = 0" ``` lp15@70097 ` 1280` ``` by (simp add: zero_def enorm_def) ``` lp15@70097 ` 1281` ``` have cm_enorm: "continuous_map ?E euclideanreal enorm" ``` lp15@70097 ` 1282` ``` unfolding enorm_def ``` lp15@70097 ` 1283` ``` proof (intro continuous_intros) ``` lp15@70097 ` 1284` ``` show "continuous_map ?E euclideanreal (\x. x i)" ``` lp15@70097 ` 1285` ``` if "i \ {.. enorm x" for x ``` lp15@70097 ` 1289` ``` by (auto simp: enorm_def sum_nonneg) ``` lp15@70097 ` 1290` ``` have le_enorm: "\x i\ \ enorm x" if "i < n" for i x ``` lp15@70097 ` 1291` ``` proof - ``` lp15@70097 ` 1292` ``` have "\x i\ \ sqrt (\k\{i}. (x k)\<^sup>2)" ``` lp15@70097 ` 1293` ``` by auto ``` lp15@70097 ` 1294` ``` also have "\ \ sqrt (\k2)" ``` lp15@70097 ` 1295` ``` by (rule real_sqrt_le_mono [OF sum_mono2]) (use that in auto) ``` lp15@70097 ` 1296` ``` finally show ?thesis ``` lp15@70097 ` 1297` ``` by (simp add: enorm_def) ``` lp15@70097 ` 1298` ``` qed ``` lp15@70097 ` 1299` ``` define B where "B \ \r. {x \ topspace ?E. enorm x < r}" ``` lp15@70097 ` 1300` ``` define C where "C \ \r. {x \ topspace ?E. enorm x \ r}" ``` lp15@70097 ` 1301` ``` define S where "S \ \r. {x \ topspace ?E. enorm x = r}" ``` lp15@70097 ` 1302` ``` have BC: "B r \ C r" and SC: "S r \ C r" and disjSB: "disjnt (S r) (B r)" and eqC: "B r \ S r = C r" for r ``` lp15@70097 ` 1303` ``` by (auto simp: B_def C_def S_def disjnt_def) ``` lp15@70097 ` 1304` ``` consider "n = 1" | "n \ 2" ``` lp15@70097 ` 1305` ``` using False by linarith ``` lp15@70097 ` 1306` ``` then have **: "openin ?E (h ` (B r))" ``` lp15@70097 ` 1307` ``` if "r > 0" and cmh: "continuous_map(subtopology ?E (C r)) ?E h" and injh: "inj_on h (C r)" for r h ``` lp15@70097 ` 1308` ``` proof cases ``` lp15@70097 ` 1309` ``` case 1 ``` lp15@70097 ` 1310` ``` define e :: "[real,nat]\real" where "e \ \x i. if i = 0 then x else 0" ``` lp15@70097 ` 1311` ``` define e' :: "(nat\real)\real" where "e' \ \x. x 0" ``` lp15@70097 ` 1312` ``` have "continuous_map euclidean euclideanreal (\f. f (0::nat))" ``` lp15@70097 ` 1313` ``` by auto ``` lp15@70097 ` 1314` ``` then have "continuous_map (subtopology (powertop_real UNIV) {f. \n\Suc 0. f n = 0}) euclideanreal (\f. f 0)" ``` lp15@70097 ` 1315` ``` by (metis (mono_tags) continuous_map_from_subtopology euclidean_product_topology) ``` lp15@70097 ` 1316` ``` then have hom_ee': "homeomorphic_maps euclideanreal (Euclidean_space 1) e e'" ``` lp15@70097 ` 1317` ``` by (auto simp: homeomorphic_maps_def e_def e'_def continuous_map_in_subtopology Euclidean_space_def) ``` lp15@70097 ` 1318` ``` have eBr: "e ` {-r<..x. x * _"] cong: if_cong) ``` lp15@70097 ` 1321` ``` have in_Cr: "\x. \-r < x; x < r\ \ (\i. if i = 0 then x else 0) \ C r" ``` lp15@70097 ` 1322` ``` using \n \ 0\ by (auto simp: C_def topspace_Euclidean_space) ``` lp15@70097 ` 1323` ``` have inj: "inj_on (e' \ h \ e) {- r<..i. if i = 0 then x else 0) 0 = h (\i. if i = 0 then y else 0) 0" ``` lp15@70097 ` 1327` ``` and "-r < x" "x < r" "-r < y" "y < r" ``` lp15@70097 ` 1328` ``` for x y :: real ``` lp15@70097 ` 1329` ``` proof - ``` lp15@70097 ` 1330` ``` have x: "(\i. if i = 0 then x else 0) \ C r" and y: "(\i. if i = 0 then y else 0) \ C r" ``` lp15@70097 ` 1331` ``` by (blast intro: inj_onD [OF \inj_on h (C r)\] that in_Cr)+ ``` lp15@70097 ` 1332` ``` have "continuous_map (subtopology (Euclidean_space (Suc 0)) (C r)) (Euclidean_space (Suc 0)) h" ``` lp15@70097 ` 1333` ``` using cmh by (simp add: 1) ``` lp15@70097 ` 1334` ``` then have "h ` ({x. \i\Suc 0. x i = 0} \ C r) \ {x. \i\Suc 0. x i = 0}" ``` lp15@70097 ` 1335` ``` by (force simp: Euclidean_space_def subtopology_subtopology continuous_map_def) ``` lp15@70097 ` 1336` ``` have "h (\i. if i = 0 then x else 0) j = h (\i. if i = 0 then y else 0) j" for j ``` lp15@70097 ` 1337` ``` proof (cases j) ``` lp15@70097 ` 1338` ``` case (Suc j') ``` lp15@70097 ` 1339` ``` have "h ` ({x. \i\Suc 0. x i = 0} \ C r) \ {x. \i\Suc 0. x i = 0}" ``` lp15@70097 ` 1340` ``` using continuous_map_image_subset_topspace [OF cmh] ``` lp15@70097 ` 1341` ``` by (simp add: 1 Euclidean_space_def subtopology_subtopology) ``` lp15@70097 ` 1342` ``` with Suc f x y show ?thesis ``` lp15@70097 ` 1343` ``` by (simp add: "1" image_subset_iff) ``` lp15@70097 ` 1344` ``` qed (use f in blast) ``` lp15@70097 ` 1345` ``` then have "(\i. if i = 0 then x else 0) = (\i::nat. if i = 0 then y else 0)" ``` lp15@70097 ` 1346` ``` by (blast intro: inj_onD [OF \inj_on h (C r)\] that in_Cr) ``` lp15@70097 ` 1347` ``` then show ?thesis ``` lp15@70097 ` 1348` ``` by (simp add: fun_eq_iff) presburger ``` lp15@70097 ` 1349` ``` qed ``` lp15@70097 ` 1350` ``` qed ``` lp15@70097 ` 1351` ``` have hom_e': "homeomorphic_map (Euclidean_space 1) euclideanreal e'" ``` lp15@70097 ` 1352` ``` using hom_ee' homeomorphic_maps_map by blast ``` lp15@70097 ` 1353` ``` have "openin (Euclidean_space n) (h ` e ` {- r<.. topspace (Euclidean_space 1)" ``` lp15@70097 ` 1357` ``` using "1" C_def \\r. B r \ C r\ cmh continuous_map_image_subset_topspace eBr by fastforce ``` lp15@70097 ` 1358` ``` have cont: "continuous_on {- r<.. h \ e)" ``` lp15@70097 ` 1359` ``` proof (intro continuous_on_compose) ``` lp15@70097 ` 1360` ``` have "\i. continuous_on {- r<..x. if i = 0 then x else 0)" ``` lp15@70097 ` 1361` ``` by (auto simp: continuous_on_topological) ``` lp15@70097 ` 1362` ``` then show "continuous_on {- r<.. topspace (subtopology ?E (C r))" ``` lp15@70097 ` 1365` ``` by (auto simp: eBr \\r. B r \ C r\) (auto simp: B_def) ``` lp15@70097 ` 1366` ``` with cmh show "continuous_on (e ` {- r<.. topspace ?E" ``` lp15@70097 ` 1369` ``` using subCr cmh by (simp add: continuous_map_def image_subset_iff) ``` lp15@70097 ` 1370` ``` moreover have "continuous_on (topspace ?E) e'" ``` lp15@70097 ` 1371` ``` by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def) ``` lp15@70097 ` 1372` ``` ultimately show "continuous_on (h ` e ` {- r<..r. closedin (Euclidean_space n) (C r)" ``` lp15@70097 ` 1383` ``` unfolding C_def ``` lp15@70097 ` 1384` ``` by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl: "{.._}", simplified]) ``` lp15@70097 ` 1385` ``` have cloS: "\r. closedin (Euclidean_space n) (S r)" ``` lp15@70097 ` 1386` ``` unfolding S_def ``` lp15@70097 ` 1387` ``` by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl: "{_}", simplified]) ``` lp15@70097 ` 1388` ``` have C_subset: "C r \ UNIV \\<^sub>E {- \r\..\r\}" ``` lp15@70097 ` 1389` ``` using le_enorm \r > 0\ ``` lp15@70097 ` 1390` ``` apply (auto simp: C_def topspace_Euclidean_space abs_le_iff) ``` lp15@70097 ` 1391` ``` apply (metis add.inverse_neutral le_cases less_minus_iff not_le order_trans) ``` lp15@70097 ` 1392` ``` by (metis enorm_ge0 not_le order.trans) ``` lp15@70097 ` 1393` ``` have compactinC: "compactin (Euclidean_space n) (C r)" ``` lp15@70097 ` 1394` ``` unfolding Euclidean_space_def compactin_subtopology ``` lp15@70097 ` 1395` ``` proof ``` lp15@70097 ` 1396` ``` show "compactin (powertop_real UNIV) (C r)" ``` lp15@70097 ` 1397` ``` proof (rule closed_compactin [OF _ C_subset]) ``` lp15@70097 ` 1398` ``` show "closedin (powertop_real UNIV) (C r)" ``` lp15@70097 ` 1399` ``` by (metis Euclidean_space_def cloC closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space) ``` lp15@70097 ` 1400` ``` qed (simp add: compactin_PiE) ``` lp15@70097 ` 1401` ``` qed (auto simp: C_def topspace_Euclidean_space) ``` lp15@70097 ` 1402` ``` have compactinS: "compactin (Euclidean_space n) (S r)" ``` lp15@70097 ` 1403` ``` unfolding Euclidean_space_def compactin_subtopology ``` lp15@70097 ` 1404` ``` proof ``` lp15@70097 ` 1405` ``` show "compactin (powertop_real UNIV) (S r)" ``` lp15@70097 ` 1406` ``` proof (rule closed_compactin) ``` lp15@70097 ` 1407` ``` show "S r \ UNIV \\<^sub>E {- \r\..\r\}" ``` lp15@70097 ` 1408` ``` using C_subset \\r. S r \ C r\ by blast ``` lp15@70097 ` 1409` ``` show "closedin (powertop_real UNIV) (S r)" ``` lp15@70097 ` 1410` ``` by (metis Euclidean_space_def cloS closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space) ``` lp15@70097 ` 1411` ``` qed (simp add: compactin_PiE) ``` lp15@70097 ` 1412` ``` qed (auto simp: S_def topspace_Euclidean_space) ``` lp15@70097 ` 1413` ``` have h_if_B: "\y. y \ B r \ h y \ topspace ?E" ``` lp15@70097 ` 1414` ``` using B_def \\r. B r \ S r = C r\ cmh continuous_map_image_subset_topspace by fastforce ``` lp15@70097 ` 1415` ``` have com_hSr: "compactin (Euclidean_space n) (h ` S r)" ``` lp15@70097 ` 1416` ``` by (meson \\r. S r \ C r\ cmh compactinS compactin_subtopology image_compactin) ``` lp15@70097 ` 1417` ``` have ope_comp_hSr: "openin (Euclidean_space n) (topspace (Euclidean_space n) - h ` S r)" ``` lp15@70097 ` 1418` ``` proof (rule openin_diff) ``` lp15@70097 ` 1419` ``` show "closedin (Euclidean_space n) (h ` S r)" ``` lp15@70097 ` 1420` ``` using Hausdorff_Euclidean_space com_hSr compactin_imp_closedin by blast ``` lp15@70097 ` 1421` ``` qed auto ``` lp15@70097 ` 1422` ``` have h_pcs: "h ` (B r) \ path_components_of (subtopology ?E (topspace ?E - h ` (S r)))" ``` lp15@70097 ` 1423` ``` proof (rule lemmaIOD) ``` lp15@70097 ` 1424` ``` have pc_interval: "path_connectedin (Euclidean_space n) {x \ topspace(Euclidean_space n). enorm x \ T}" ``` lp15@70097 ` 1425` ``` if T: "is_interval T" for T ``` lp15@70097 ` 1426` ``` proof - ``` lp15@70097 ` 1427` ``` define mul :: "[real, nat \ real, nat] \ real" where "mul \ \a x i. a * x i" ``` lp15@70097 ` 1428` ``` let ?neg = "mul (-1)" ``` lp15@70097 ` 1429` ``` have neg_neg [simp]: "?neg (?neg x) = x" for x ``` lp15@70097 ` 1430` ``` by (simp add: mul_def) ``` lp15@70097 ` 1431` ``` have enorm_mul [simp]: "enorm(mul a x) = abs a * enorm x" for a x ``` lp15@70097 ` 1432` ``` by (simp add: enorm_def mul_def power_mult_distrib) (metis real_sqrt_abs real_sqrt_mult sum_distrib_left) ``` lp15@70097 ` 1433` ``` have mul_in_top: "mul a x \ topspace ?E" ``` lp15@70097 ` 1434` ``` if "x \ topspace ?E" for a x ``` lp15@70097 ` 1435` ``` using mul_def that topspace_Euclidean_space by auto ``` lp15@70097 ` 1436` ``` have neg_in_S: "?neg x \ S r" ``` lp15@70097 ` 1437` ``` if "x \ S r" for x r ``` lp15@70097 ` 1438` ``` using that topspace_Euclidean_space S_def by simp (simp add: mul_def) ``` lp15@70097 ` 1439` ``` have *: "path_connectedin ?E (S d)" ``` lp15@70097 ` 1440` ``` if "d \ 0" for d ``` lp15@70097 ` 1441` ``` proof (cases "d = 0") ``` lp15@70097 ` 1442` ``` let ?ES = "subtopology ?E (S d)" ``` lp15@70097 ` 1443` ``` case False ``` lp15@70097 ` 1444` ``` then have "d > 0" ``` lp15@70097 ` 1445` ``` using that by linarith ``` lp15@70097 ` 1446` ``` moreover have "path_connected_space ?ES" ``` lp15@70097 ` 1447` ``` unfolding path_connected_space_iff_path_component ``` lp15@70097 ` 1448` ``` proof clarify ``` lp15@70097 ` 1449` ``` have **: "path_component_of ?ES x y" ``` lp15@70097 ` 1450` ``` if x: "x \ topspace ?ES" and y: "y \ topspace ?ES" "x \ ?neg y" for x y ``` lp15@70097 ` 1451` ``` proof - ``` lp15@70097 ` 1452` ``` show ?thesis ``` lp15@70097 ` 1453` ``` unfolding path_component_of_def pathin_def S_def ``` lp15@70097 ` 1454` ``` proof (intro exI conjI) ``` lp15@70097 ` 1455` ``` let ?g = "(\x. mul (d / enorm x) x) \ (\t i. (1 - t) * x i + t * y i)" ``` lp15@70097 ` 1456` ``` show "continuous_map (top_of_set {0::real..1}) (subtopology ?E {x \ topspace ?E. enorm x = d}) ?g" ``` lp15@70097 ` 1457` ``` proof (rule continuous_map_compose) ``` lp15@70097 ` 1458` ``` let ?Y = "subtopology ?E (- {zero})" ``` lp15@70097 ` 1459` ``` have **: False ``` lp15@70097 ` 1460` ``` if eq0: "\j. (1 - r) * x j + r * y j = 0" ``` lp15@70097 ` 1461` ``` and ne: "x i \ - y i" ``` lp15@70097 ` 1462` ``` and d: "enorm x = d" "enorm y = d" ``` lp15@70097 ` 1463` ``` and r: "0 \ r" "r \ 1" ``` lp15@70097 ` 1464` ``` for i r ``` lp15@70097 ` 1465` ``` proof - ``` lp15@70097 ` 1466` ``` have "mul (1-r) x = ?neg (mul r y)" ``` lp15@70097 ` 1467` ``` using eq0 by (simp add: mul_def fun_eq_iff algebra_simps) ``` lp15@70097 ` 1468` ``` then have "enorm (mul (1-r) x) = enorm (?neg (mul r y))" ``` lp15@70097 ` 1469` ``` by metis ``` lp15@70097 ` 1470` ``` with r have "(1-r) * enorm x = r * enorm y" ``` lp15@70097 ` 1471` ``` by simp ``` lp15@70097 ` 1472` ``` then have r12: "r = 1/2" ``` lp15@70097 ` 1473` ``` using \d \ 0\ d by auto ``` lp15@70097 ` 1474` ``` show ?thesis ``` lp15@70097 ` 1475` ``` using ne eq0 [of i] unfolding r12 by (simp add: algebra_simps) ``` lp15@70097 ` 1476` ``` qed ``` lp15@70097 ` 1477` ``` show "continuous_map (top_of_set {0..1}) ?Y (\t i. (1 - t) * x i + t * y i)" ``` lp15@70097 ` 1478` ``` using x y ``` lp15@70097 ` 1479` ``` unfolding continuous_map_componentwise_UNIV Euclidean_space_def continuous_map_in_subtopology ``` lp15@70097 ` 1480` ``` apply (intro conjI allI continuous_intros) ``` lp15@70097 ` 1481` ``` apply (auto simp: zero_def mul_def S_def Euclidean_space_def fun_eq_iff) ``` lp15@70097 ` 1482` ``` using ** by blast ``` lp15@70097 ` 1483` ``` have cm_enorm': "continuous_map (subtopology (powertop_real UNIV) A) euclideanreal enorm" for A ``` lp15@70097 ` 1484` ``` unfolding enorm_def by (intro continuous_intros) auto ``` lp15@70097 ` 1485` ``` have "continuous_map ?Y (subtopology ?E {x. enorm x = d}) (\x. mul (d / enorm x) x)" ``` lp15@70097 ` 1486` ``` unfolding continuous_map_in_subtopology ``` lp15@70097 ` 1487` ``` proof (intro conjI) ``` lp15@70097 ` 1488` ``` show "continuous_map ?Y (Euclidean_space n) (\x. mul (d / enorm x) x)" ``` lp15@70097 ` 1489` ``` unfolding continuous_map_in_subtopology Euclidean_space_def mul_def zero_def subtopology_subtopology continuous_map_componentwise_UNIV ``` lp15@70097 ` 1490` ``` proof (intro conjI allI cm_enorm' continuous_intros) ``` lp15@70097 ` 1491` ``` show "enorm x \ 0" ``` lp15@70097 ` 1492` ``` if "x \ topspace (subtopology (powertop_real UNIV) ({x. \i\n. x i = 0} \ - {\i. 0}))" for x ``` lp15@70097 ` 1493` ``` using that by simp (metis abs_le_zero_iff le_enorm not_less) ``` lp15@70097 ` 1494` ``` qed auto ``` lp15@70097 ` 1495` ``` qed (use \d > 0\ enorm_ge0 in auto) ``` lp15@70097 ` 1496` ``` moreover have "subtopology ?E {x \ topspace ?E. enorm x = d} = subtopology ?E {x. enorm x = d}" ``` lp15@70097 ` 1497` ``` by (simp add: subtopology_restrict Collect_conj_eq) ``` lp15@70097 ` 1498` ``` ultimately show "continuous_map ?Y (subtopology (Euclidean_space n) {x \ topspace (Euclidean_space n). enorm x = d}) (\x. mul (d / enorm x) x)" ``` lp15@70097 ` 1499` ``` by metis ``` lp15@70097 ` 1500` ``` qed ``` lp15@70097 ` 1501` ``` show "?g (0::real) = x" "?g (1::real) = y" ``` lp15@70097 ` 1502` ``` using that by (auto simp: S_def zero_def mul_def fun_eq_iff) ``` lp15@70097 ` 1503` ``` qed ``` lp15@70097 ` 1504` ``` qed ``` lp15@70097 ` 1505` ``` obtain a b where a: "a \ topspace ?ES" and b: "b \ topspace ?ES" ``` lp15@70097 ` 1506` ``` and "a \ b" and negab: "?neg a \ b" ``` lp15@70097 ` 1507` ``` proof ``` lp15@70097 ` 1508` ``` let ?v = "\j i::nat. if i = j then d else 0" ``` lp15@70097 ` 1509` ``` show "?v 0 \ topspace (subtopology ?E (S d))" "?v 1 \ topspace (subtopology ?E (S d))" ``` lp15@70097 ` 1510` ``` using \n \ 2\ \d \ 0\ by (auto simp: S_def topspace_Euclidean_space) ``` lp15@70097 ` 1511` ``` show "?v 0 \ ?v 1" "?neg (?v 0) \ (?v 1)" ``` lp15@70097 ` 1512` ``` using \d > 0\ by (auto simp: mul_def fun_eq_iff) ``` lp15@70097 ` 1513` ``` qed ``` lp15@70097 ` 1514` ``` show "path_component_of ?ES x y" ``` lp15@70097 ` 1515` ``` if x: "x \ topspace ?ES" and y: "y \ topspace ?ES" ``` lp15@70097 ` 1516` ``` for x y ``` lp15@70097 ` 1517` ``` proof - ``` lp15@70097 ` 1518` ``` have "path_component_of ?ES x (?neg x)" ``` lp15@70097 ` 1519` ``` proof - ``` lp15@70097 ` 1520` ``` have "path_component_of ?ES x a" ``` lp15@70097 ` 1521` ``` by (metis (no_types, hide_lams) ** a b \a \ b\ negab path_component_of_trans path_component_of_sym x) ``` lp15@70097 ` 1522` ``` moreover ``` lp15@70097 ` 1523` ``` have pa_ab: "path_component_of ?ES a b" using "**" a b negab neg_neg by blast ``` lp15@70097 ` 1524` ``` then have "path_component_of ?ES a (?neg x)" ``` lp15@70097 ` 1525` ``` by (metis "**" \a \ b\ cloS closedin_def neg_in_S path_component_of_equiv topspace_subtopology_subset x) ``` lp15@70097 ` 1526` ``` ultimately show ?thesis ``` lp15@70097 ` 1527` ``` by (meson path_component_of_trans) ``` lp15@70097 ` 1528` ``` qed ``` lp15@70097 ` 1529` ``` then show ?thesis ``` lp15@70097 ` 1530` ``` using "**" x y by force ``` lp15@70097 ` 1531` ``` qed ``` lp15@70097 ` 1532` ``` qed ``` lp15@70097 ` 1533` ``` ultimately show ?thesis ``` lp15@70097 ` 1534` ``` by (simp add: cloS closedin_subset path_connectedin_def) ``` lp15@70097 ` 1535` ``` qed (simp add: S_def cong: conj_cong) ``` lp15@70097 ` 1536` ``` have "path_component_of (subtopology ?E {x \ topspace ?E. enorm x \ T}) x y" ``` lp15@70097 ` 1537` ``` if "enorm x = a" "x \ topspace ?E" "enorm x \ T" "enorm y = b" "y \ topspace ?E" "enorm y \ T" ``` lp15@70097 ` 1538` ``` for x y a b ``` lp15@70097 ` 1539` ``` using that ``` lp15@70097 ` 1540` ``` proof (induction a b arbitrary: x y rule: linorder_less_wlog) ``` lp15@70097 ` 1541` ``` case (less a b) ``` lp15@70097 ` 1542` ``` then have "a \ 0" ``` lp15@70097 ` 1543` ``` using enorm_ge0 by blast ``` lp15@70097 ` 1544` ``` with less.hyps have "b > 0" ``` lp15@70097 ` 1545` ``` by linarith ``` lp15@70097 ` 1546` ``` show ?case ``` lp15@70097 ` 1547` ``` proof (rule path_component_of_trans) ``` lp15@70097 ` 1548` ``` have y'_ts: "mul (a / b) y \ topspace ?E" ``` lp15@70097 ` 1549` ``` using \y \ topspace ?E\ mul_in_top by blast ``` lp15@70097 ` 1550` ``` moreover have "enorm (mul (a / b) y) = a" ``` lp15@70097 ` 1551` ``` unfolding enorm_mul using \0 < b\ \0 \ a\ less.prems by simp ``` lp15@70097 ` 1552` ``` ultimately have y'_S: "mul (a / b) y \ S a" ``` lp15@70097 ` 1553` ``` using S_def by blast ``` lp15@70097 ` 1554` ``` have "x \ S a" ``` lp15@70097 ` 1555` ``` using S_def less.prems by blast ``` lp15@70097 ` 1556` ``` with \x \ topspace ?E\ y'_ts y'_S ``` lp15@70097 ` 1557` ``` have "path_component_of (subtopology ?E (S a)) x (mul (a / b) y)" ``` lp15@70097 ` 1558` ``` by (metis * [OF \a \ 0\] path_connected_space_iff_path_component path_connectedin_def topspace_subtopology_subset) ``` lp15@70097 ` 1559` ``` moreover ``` lp15@70097 ` 1560` ``` have "{f \ topspace ?E. enorm f = a} \ {f \ topspace ?E. enorm f \ T}" ``` lp15@70097 ` 1561` ``` using \enorm x = a\ \enorm x \ T\ by force ``` lp15@70097 ` 1562` ``` ultimately ``` lp15@70097 ` 1563` ``` show "path_component_of (subtopology ?E {x. x \ topspace ?E \ enorm x \ T}) x (mul (a / b) y)" ``` lp15@70097 ` 1564` ``` by (simp add: S_def path_component_of_mono) ``` lp15@70097 ` 1565` ``` have "pathin ?E (\t. mul (((1 - t) * b + t * a) / b) y)" ``` lp15@70097 ` 1566` ``` using \b > 0\ \y \ topspace ?E\ ``` lp15@70097 ` 1567` ``` unfolding pathin_def Euclidean_space_def mul_def continuous_map_in_subtopology continuous_map_componentwise_UNIV ``` lp15@70097 ` 1568` ``` by (intro allI conjI continuous_intros) auto ``` lp15@70097 ` 1569` ``` moreover have "mul (((1 - t) * b + t * a) / b) y \ topspace ?E" ``` lp15@70097 ` 1570` ``` if "t \ {0..1}" for t ``` lp15@70097 ` 1571` ``` using \y \ topspace ?E\ mul_in_top by blast ``` lp15@70097 ` 1572` ``` moreover have "enorm (mul (((1 - t) * b + t * a) / b) y) \ T" ``` lp15@70097 ` 1573` ``` if "t \ {0..1}" for t ``` lp15@70097 ` 1574` ``` proof - ``` lp15@70097 ` 1575` ``` have "a \ T" "b \ T" ``` lp15@70097 ` 1576` ``` using less.prems by auto ``` lp15@70097 ` 1577` ``` then have "\(1 - t) * b + t * a\ \ T" ``` lp15@70097 ` 1578` ``` proof (rule mem_is_interval_1_I [OF T]) ``` lp15@70097 ` 1579` ``` show "a \ \(1 - t) * b + t * a\" ``` lp15@70097 ` 1580` ``` using that \a \ 0\ less.hyps segment_bound_lemma by auto ``` lp15@70097 ` 1581` ``` show "\(1 - t) * b + t * a\ \ b" ``` lp15@70097 ` 1582` ``` using that \a \ 0\ less.hyps by (auto intro: convex_bound_le) ``` lp15@70097 ` 1583` ``` qed ``` lp15@70097 ` 1584` ``` then show ?thesis ``` lp15@70097 ` 1585` ``` unfolding enorm_mul \enorm y = b\ using that \b > 0\ by simp ``` lp15@70097 ` 1586` ``` qed ``` lp15@70097 ` 1587` ``` ultimately have pa: "pathin (subtopology ?E {x \ topspace ?E. enorm x \ T}) ``` lp15@70097 ` 1588` ``` (\t. mul (((1 - t) * b + t * a) / b) y)" ``` lp15@70097 ` 1589` ``` by (auto simp: pathin_subtopology) ``` lp15@70097 ` 1590` ``` have ex_pathin: "\g. pathin (subtopology ?E {x \ topspace ?E. enorm x \ T}) g \ ``` lp15@70097 ` 1591` ``` g 0 = y \ g 1 = mul (a / b) y" ``` lp15@70097 ` 1592` ``` apply (rule_tac x="\t. mul (((1 - t) * b + t * a) / b) y" in exI) ``` lp15@70097 ` 1593` ``` using \b > 0\ pa by (auto simp: mul_def) ``` lp15@70097 ` 1594` ``` show "path_component_of (subtopology ?E {x. x \ topspace ?E \ enorm x \ T}) (mul (a / b) y) y" ``` lp15@70097 ` 1595` ``` by (rule path_component_of_sym) (simp add: path_component_of_def ex_pathin) ``` lp15@70097 ` 1596` ``` qed ``` lp15@70097 ` 1597` ``` next ``` lp15@70097 ` 1598` ``` case (refl a) ``` lp15@70097 ` 1599` ``` then have pc: "path_component_of (subtopology ?E (S (enorm u))) u v" ``` lp15@70097 ` 1600` ``` if "u \ topspace ?E \ S (enorm x)" "v \ topspace ?E \ S (enorm u)" for u v ``` lp15@70097 ` 1601` ``` using * [of a] enorm_ge0 that ``` lp15@70097 ` 1602` ``` by (auto simp: path_connectedin_def path_connected_space_iff_path_component S_def) ``` lp15@70097 ` 1603` ``` have sub: "{u \ topspace ?E. enorm u = enorm x} \ {u \ topspace ?E. enorm u \ T}" ``` lp15@70097 ` 1604` ``` using \enorm x \ T\ by auto ``` lp15@70097 ` 1605` ``` show ?case ``` lp15@70097 ` 1606` ``` using pc [of x y] refl by (auto simp: S_def path_component_of_mono [OF _ sub]) ``` lp15@70097 ` 1607` ``` next ``` lp15@70097 ` 1608` ``` case (sym a b) ``` lp15@70097 ` 1609` ``` then show ?case ``` lp15@70097 ` 1610` ``` by (blast intro: path_component_of_sym) ``` lp15@70097 ` 1611` ``` qed ``` lp15@70097 ` 1612` ``` then show ?thesis ``` lp15@70097 ` 1613` ``` by (simp add: path_connectedin_def path_connected_space_iff_path_component) ``` lp15@70097 ` 1614` ``` qed ``` lp15@70097 ` 1615` ``` have "h ` S r \ topspace ?E" ``` lp15@70097 ` 1616` ``` by (meson SC cmh compact_imp_compactin_subtopology compactinS compactin_subset_topspace image_compactin) ``` lp15@70097 ` 1617` ``` moreover ``` lp15@70097 ` 1618` ``` have "\ compact_space ?E " ``` lp15@70097 ` 1619` ``` by (metis compact_Euclidean_space \n \ 0\) ``` lp15@70097 ` 1620` ``` then have "\ compactin ?E (topspace ?E)" ``` lp15@70097 ` 1621` ``` by (simp add: compact_space_def topspace_Euclidean_space) ``` lp15@70097 ` 1622` ``` then have "h ` S r \ topspace ?E" ``` lp15@70097 ` 1623` ``` using com_hSr by auto ``` lp15@70097 ` 1624` ``` ultimately have top_hSr_ne: "topspace (subtopology ?E (topspace ?E - h ` S r)) \ {}" ``` lp15@70097 ` 1625` ``` by auto ``` lp15@70097 ` 1626` ``` show pc1: "\T. T \ path_components_of (subtopology ?E (topspace ?E - h ` S r)) \ h ` B r \ T" ``` lp15@70097 ` 1627` ``` proof (rule exists_path_component_of_superset [OF _ top_hSr_ne]) ``` lp15@70097 ` 1628` ``` have "path_connectedin ?E (h ` B r)" ``` lp15@70097 ` 1629` ``` proof (rule path_connectedin_continuous_map_image) ``` lp15@70097 ` 1630` ``` show "continuous_map (subtopology ?E (C r)) ?E h" ``` lp15@70097 ` 1631` ``` by (simp add: cmh) ``` lp15@70097 ` 1632` ``` have "path_connectedin ?E (B r)" ``` lp15@70097 ` 1633` ``` using pc_interval[of "{.. topspace ?E - h ` S r" ``` lp15@70097 ` 1638` ``` apply (auto simp: h_if_B) ``` lp15@70097 ` 1639` ``` by (metis BC SC disjSB disjnt_iff inj_onD [OF injh] subsetD) ``` lp15@70097 ` 1640` ``` ultimately show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (h ` B r)" ``` lp15@70097 ` 1641` ``` by (simp add: path_connectedin_subtopology) ``` lp15@70097 ` 1642` ``` qed metis ``` lp15@70097 ` 1643` ``` show "\T. T \ path_components_of (subtopology ?E (topspace ?E - h ` S r)) \ topspace ?E - h ` (C r) \ T" ``` lp15@70097 ` 1644` ``` proof (rule exists_path_component_of_superset [OF _ top_hSr_ne]) ``` lp15@70097 ` 1645` ``` have eq: "topspace ?E - {x \ topspace ?E. enorm x \ r} = {x \ topspace ?E. r < enorm x}" ``` lp15@70097 ` 1646` ``` by auto ``` lp15@70097 ` 1647` ``` have "path_connectedin ?E (topspace ?E - C r)" ``` lp15@70097 ` 1648` ``` using pc_interval[of "{r<..}"] is_interval_convex_1 unfolding C_def eq by auto ``` lp15@70097 ` 1649` ``` then have "path_connectedin ?E (topspace ?E - h ` C r)" ``` lp15@70097 ` 1650` ``` by (metis biglemma [OF \n \ 0\ compactinC cmh injh]) ``` lp15@70097 ` 1651` ``` then show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (topspace ?E - h ` C r)" ``` lp15@70097 ` 1652` ``` by (simp add: Diff_mono SC image_mono path_connectedin_subtopology) ``` lp15@70097 ` 1653` ``` qed metis ``` lp15@70097 ` 1654` ``` have "topspace ?E \ (topspace ?E - h ` S r) = h ` B r \ (topspace ?E - h ` C r)" (is "?lhs = ?rhs") ``` lp15@70097 ` 1655` ``` proof ``` lp15@70097 ` 1656` ``` show "?lhs \ ?rhs" ``` lp15@70097 ` 1657` ``` using \\r. B r \ S r = C r\ by auto ``` lp15@70097 ` 1658` ``` have "h ` B r \ h ` S r = {}" ``` lp15@70097 ` 1659` ``` by (metis Diff_triv \\r. B r \ S r = C r\ \\r. disjnt (S r) (B r)\ disjnt_def inf_commute inj_on_Un injh) ``` lp15@70097 ` 1660` ``` then show "?rhs \ ?lhs" ``` lp15@70097 ` 1661` ``` using path_components_of_subset pc1 \\r. B r \ S r = C r\ ``` lp15@70097 ` 1662` ``` by (fastforce simp add: h_if_B) ``` lp15@70097 ` 1663` ``` qed ``` lp15@70097 ` 1664` ``` then show "\ (path_components_of (subtopology ?E (topspace ?E - h ` S r))) = h ` B r \ (topspace ?E - h ` (C r))" ``` lp15@70097 ` 1665` ``` by (simp add: Union_path_components_of) ``` lp15@70097 ` 1666` ``` show "T \ {}" ``` lp15@70097 ` 1667` ``` if "T \ path_components_of (subtopology ?E (topspace ?E - h ` S r))" for T ``` lp15@70097 ` 1668` ``` using that by (simp add: nonempty_path_components_of) ``` lp15@70097 ` 1669` ``` show "disjoint (path_components_of (subtopology ?E (topspace ?E - h ` S r)))" ``` lp15@70097 ` 1670` ``` by (simp add: pairwise_disjoint_path_components_of) ``` lp15@70097 ` 1671` ``` have "\ path_connectedin ?E (topspace ?E - h ` S r)" ``` lp15@70097 ` 1672` ``` proof (subst biglemma [OF \n \ 0\ compactinS]) ``` lp15@70097 ` 1673` ``` show "continuous_map (subtopology ?E (S r)) ?E h" ``` lp15@70097 ` 1674` ``` by (metis Un_commute Un_upper1 cmh continuous_map_from_subtopology_mono eqC) ``` lp15@70097 ` 1675` ``` show "inj_on h (S r)" ``` lp15@70097 ` 1676` ``` using SC inj_on_subset injh by blast ``` lp15@70097 ` 1677` ``` show "\ path_connectedin ?E (topspace ?E - S r)" ``` lp15@70097 ` 1678` ``` proof ``` lp15@70097 ` 1679` ``` have "topspace ?E - S r = {x \ topspace ?E. enorm x \ r}" ``` lp15@70097 ` 1680` ``` by (auto simp: S_def) ``` lp15@70097 ` 1681` ``` moreover have "enorm ` {x \ topspace ?E. enorm x \ r} = {0..} - {r}" ``` lp15@70097 ` 1682` ``` proof ``` lp15@70097 ` 1683` ``` have "\x. x \ topspace ?E \ enorm x \ r \ d = enorm x" ``` lp15@70097 ` 1684` ``` if "d \ r" "d \ 0" for d ``` lp15@70097 ` 1685` ``` proof (intro exI conjI) ``` lp15@70097 ` 1686` ``` show "(\i. if i = 0 then d else 0) \ topspace ?E" ``` lp15@70097 ` 1687` ``` using \n \ 0\ by (auto simp: Euclidean_space_def) ``` lp15@70097 ` 1688` ``` show "enorm (\i. if i = 0 then d else 0) \ r" "d = enorm (\i. if i = 0 then d else 0)" ``` lp15@70097 ` 1689` ``` using \n \ 0\ that by simp_all ``` lp15@70097 ` 1690` ``` qed ``` lp15@70097 ` 1691` ``` then show "{0..} - {r} \ enorm ` {x \ topspace ?E. enorm x \ r}" ``` lp15@70097 ` 1692` ``` by (auto simp: image_def) ``` lp15@70097 ` 1693` ``` qed (auto simp: enorm_ge0) ``` lp15@70097 ` 1694` ``` ultimately have non_r: "enorm ` (topspace ?E - S r) = {0..} - {r}" ``` lp15@70097 ` 1695` ``` by simp ``` lp15@70097 ` 1696` ``` have "\x\0. x \ r \ r \ x" ``` lp15@70097 ` 1697` ``` by (metis gt_ex le_cases not_le order_trans) ``` lp15@70097 ` 1698` ``` then have "\ is_interval ({0..} - {r})" ``` lp15@70097 ` 1699` ``` unfolding is_interval_1 ``` lp15@70097 ` 1700` ``` using \r > 0\ by (auto simp: Bex_def) ``` lp15@70097 ` 1701` ``` then show False ``` lp15@70097 ` 1702` ``` if "path_connectedin ?E (topspace ?E - S r)" ``` lp15@70097 ` 1703` ``` using path_connectedin_continuous_map_image [OF cm_enorm that] by (simp add: is_interval_path_connected_1 non_r) ``` lp15@70097 ` 1704` ``` qed ``` lp15@70097 ` 1705` ``` qed ``` lp15@70097 ` 1706` ``` then have "\ path_connected_space (subtopology ?E (topspace ?E - h ` S r))" ``` lp15@70097 ` 1707` ``` by (simp add: path_connectedin_def) ``` lp15@70097 ` 1708` ``` then show "\T. path_components_of (subtopology ?E (topspace ?E - h ` S r)) \ {T}" ``` lp15@70097 ` 1709` ``` by (simp add: path_components_of_subset_singleton) ``` lp15@70097 ` 1710` ``` qed ``` lp15@70097 ` 1711` ``` moreover have "openin ?E A" ``` lp15@70097 ` 1712` ``` if "A \ path_components_of (subtopology ?E (topspace ?E - h ` (S r)))" for A ``` lp15@70097 ` 1713` ``` using locally_path_connected_Euclidean_space [of n] that ope_comp_hSr ``` lp15@70097 ` 1714` ``` by (simp add: locally_path_connected_space_open_path_components) ``` lp15@70097 ` 1715` ``` ultimately show ?thesis by metis ``` lp15@70097 ` 1716` ``` qed ``` lp15@70097 ` 1717` ``` have "\T. openin ?E T \ f x \ T \ T \ f ` U" ``` lp15@70097 ` 1718` ``` if "x \ U" for x ``` lp15@70097 ` 1719` ``` proof - ``` lp15@70097 ` 1720` ``` have x: "x \ topspace ?E" ``` lp15@70097 ` 1721` ``` by (meson U in_mono openin_subset that) ``` lp15@70097 ` 1722` ``` obtain V where V: "openin (powertop_real UNIV) V" and Ueq: "U = V \ {x. \i\n. x i = 0}" ``` lp15@70097 ` 1723` ``` using U by (auto simp: openin_subtopology Euclidean_space_def) ``` lp15@70097 ` 1724` ``` with \x \ U\ have "x \ V" by blast ``` lp15@70097 ` 1725` ``` then obtain T where Tfin: "finite {i. T i \ UNIV}" and Topen: "\i. open (T i)" ``` lp15@70097 ` 1726` ``` and Tx: "x \ Pi\<^sub>E UNIV T" and TV: "Pi\<^sub>E UNIV T \ V" ``` lp15@70097 ` 1727` ``` using V by (force simp: openin_product_topology_alt) ``` lp15@70097 ` 1728` ``` have "\e>0. \x'. \x' - x i\ < e \ x' \ T i" for i ``` lp15@70097 ` 1729` ``` using Topen [of i] Tx by (auto simp: open_real) ``` lp15@70097 ` 1730` ``` then obtain \ where B0: "\i. \ i > 0" and BT: "\i x'. \x' - x i\ < \ i \ x' \ T i" ``` lp15@70097 ` 1731` ``` by metis ``` lp15@70097 ` 1732` ``` define r where "r \ Min (insert 1 (\ ` {i. T i \ UNIV}))" ``` lp15@70097 ` 1733` ``` have "r > 0" ``` lp15@70097 ` 1734` ``` by (simp add: B0 Tfin r_def) ``` lp15@70097 ` 1735` ``` have inU: "y \ U" ``` lp15@70097 ` 1736` ``` if y: "y \ topspace ?E" and yxr: "\i. i \y i - x i\ < r" for y ``` lp15@70097 ` 1737` ``` proof - ``` lp15@70097 ` 1738` ``` have "y i \ T i" for i ``` lp15@70097 ` 1739` ``` proof (cases "T i = UNIV") ``` lp15@70097 ` 1740` ``` show "y i \ T i" if "T i \ UNIV" ``` lp15@70097 ` 1741` ``` proof (cases "i < n") ``` lp15@70097 ` 1742` ``` case True ``` lp15@70097 ` 1743` ``` then show ?thesis ``` lp15@70097 ` 1744` ``` using yxr [OF True] that by (simp add: r_def BT Tfin) ``` lp15@70097 ` 1745` ``` next ``` lp15@70097 ` 1746` ``` case False ``` lp15@70097 ` 1747` ``` then show ?thesis ``` lp15@70097 ` 1748` ``` using B0 Ueq \x \ U\ topspace_Euclidean_space y by (force intro: BT) ``` lp15@70097 ` 1749` ``` qed ``` lp15@70097 ` 1750` ``` qed auto ``` lp15@70097 ` 1751` ``` with TV have "y \ V" by auto ``` lp15@70097 ` 1752` ``` then show ?thesis ``` lp15@70097 ` 1753` ``` using that by (auto simp: Ueq topspace_Euclidean_space) ``` lp15@70097 ` 1754` ``` qed ``` lp15@70097 ` 1755` ``` have xinU: "(\i. x i + y i) \ U" if "y \ C(r/2)" for y ``` lp15@70097 ` 1756` ``` proof (rule inU) ``` lp15@70097 ` 1757` ``` have y: "y \ topspace ?E" ``` lp15@70097 ` 1758` ``` using C_def that by blast ``` lp15@70097 ` 1759` ``` show "(\i. x i + y i) \ topspace ?E" ``` lp15@70097 ` 1760` ``` using x y by (simp add: topspace_Euclidean_space) ``` lp15@70097 ` 1761` ``` have "enorm y \ r/2" ``` lp15@70097 ` 1762` ``` using that by (simp add: C_def) ``` lp15@70097 ` 1763` ``` then show "\x i + y i - x i\ < r" if "i < n" for i ``` lp15@70097 ` 1764` ``` using le_enorm enorm_ge0 that \0 < r\ leI order_trans by fastforce ``` lp15@70097 ` 1765` ``` qed ``` lp15@70097 ` 1766` ``` show ?thesis ``` lp15@70097 ` 1767` ``` proof (intro exI conjI) ``` lp15@70097 ` 1768` ``` show "openin ?E ((f \ (\y i. x i + y i)) ` B (r/2))" ``` lp15@70097 ` 1769` ``` proof (rule **) ``` lp15@70097 ` 1770` ``` have "continuous_map (subtopology ?E (C(r/2))) (subtopology ?E U) (\y i. x i + y i)" ``` lp15@70097 ` 1771` ``` by (auto simp: xinU continuous_map_in_subtopology ``` lp15@70097 ` 1772` ``` intro!: continuous_intros continuous_map_Euclidean_space_add x) ``` lp15@70097 ` 1773` ``` then show "continuous_map (subtopology ?E (C(r/2))) ?E (f \ (\y i. x i + y i))" ``` lp15@70097 ` 1774` ``` by (rule continuous_map_compose) (simp add: cmf) ``` lp15@70097 ` 1775` ``` show "inj_on (f \ (\y i. x i + y i)) (C(r/2))" ``` lp15@70097 ` 1776` ``` proof (clarsimp simp add: inj_on_def C_def topspace_Euclidean_space simp del: divide_const_simps) ``` lp15@70097 ` 1777` ``` show "y' = y" ``` lp15@70097 ` 1778` ``` if ey: "enorm y \ r / 2" and ey': "enorm y' \ r / 2" ``` lp15@70097 ` 1779` ``` and y0: "\i\n. y i = 0" and y'0: "\i\n. y' i = 0" ``` lp15@70097 ` 1780` ``` and feq: "f (\i. x i + y' i) = f (\i. x i + y i)" ``` lp15@70097 ` 1781` ``` for y' y :: "nat \ real" ``` lp15@70097 ` 1782` ``` proof - ``` lp15@70097 ` 1783` ``` have "(\i. x i + y i) \ U" ``` lp15@70097 ` 1784` ``` proof (rule inU) ``` lp15@70097 ` 1785` ``` show "(\i. x i + y i) \ topspace ?E" ``` lp15@70097 ` 1786` ``` using topspace_Euclidean_space x y0 by auto ``` lp15@70097 ` 1787` ``` show "\x i + y i - x i\ < r" if "i < n" for i ``` lp15@70097 ` 1788` ``` using ey le_enorm [of _ y] \r > 0\ that by fastforce ``` lp15@70097 ` 1789` ``` qed ``` lp15@70097 ` 1790` ``` moreover have "(\i. x i + y' i) \ U" ``` lp15@70097 ` 1791` ``` proof (rule inU) ``` lp15@70097 ` 1792` ``` show "(\i. x i + y' i) \ topspace ?E" ``` lp15@70097 ` 1793` ``` using topspace_Euclidean_space x y'0 by auto ``` lp15@70097 ` 1794` ``` show "\x i + y' i - x i\ < r" if "i < n" for i ``` lp15@70097 ` 1795` ``` using ey' le_enorm [of _ y'] \r > 0\ that by fastforce ``` lp15@70097 ` 1796` ``` qed ``` lp15@70097 ` 1797` ``` ultimately have "(\i. x i + y' i) = (\i. x i + y i)" ``` lp15@70097 ` 1798` ``` using feq by (meson \inj_on f U\ inj_on_def) ``` lp15@70097 ` 1799` ``` then show ?thesis ``` lp15@70097 ` 1800` ``` by (auto simp: fun_eq_iff) ``` lp15@70097 ` 1801` ``` qed ``` lp15@70097 ` 1802` ``` qed ``` lp15@70097 ` 1803` ``` qed (simp add: \0 < r\) ``` lp15@70097 ` 1804` ``` have "x \ (\y i. x i + y i) ` B (r / 2)" ``` lp15@70097 ` 1805` ``` proof ``` lp15@70097 ` 1806` ``` show "x = (\i. x i + zero i)" ``` lp15@70097 ` 1807` ``` by (simp add: zero_def) ``` lp15@70097 ` 1808` ``` qed (auto simp: B_def \r > 0\) ``` lp15@70097 ` 1809` ``` then show "f x \ (f \ (\y i. x i + y i)) ` B (r/2)" ``` lp15@70097 ` 1810` ``` by (metis image_comp image_eqI) ``` lp15@70097 ` 1811` ``` show "(f \ (\y i. x i + y i)) ` B (r/2) \ f ` U" ``` lp15@70097 ` 1812` ``` using \\r. B r \ C r\ xinU by fastforce ``` lp15@70097 ` 1813` ``` qed ``` lp15@70097 ` 1814` ``` qed ``` lp15@70097 ` 1815` ``` then show ?thesis ``` lp15@70097 ` 1816` ``` using openin_subopen by force ``` lp15@70097 ` 1817` ```qed ``` lp15@70097 ` 1818` lp15@70097 ` 1819` lp15@70097 ` 1820` ```corollary invariance_of_domain_Euclidean_space_embedding_map: ``` lp15@70097 ` 1821` ``` assumes "openin (Euclidean_space n) U" ``` lp15@70097 ` 1822` ``` and cmf: "continuous_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f" ``` lp15@70097 ` 1823` ``` and "inj_on f U" ``` lp15@70097 ` 1824` ``` shows "embedding_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f" ``` lp15@70097 ` 1825` ```proof (rule injective_open_imp_embedding_map [OF cmf]) ``` lp15@70097 ` 1826` ``` show "open_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f" ``` lp15@70097 ` 1827` ``` unfolding open_map_def ``` lp15@70097 ` 1828` ``` by (meson assms continuous_map_from_subtopology_mono inj_on_subset invariance_of_domain_Euclidean_space openin_imp_subset openin_trans_full) ``` lp15@70097 ` 1829` ``` show "inj_on f (topspace (subtopology (Euclidean_space n) U))" ``` lp15@70097 ` 1830` ``` using assms openin_subset topspace_subtopology_subset by fastforce ``` lp15@70097 ` 1831` ```qed ``` lp15@70097 ` 1832` lp15@70097 ` 1833` ```corollary invariance_of_domain_Euclidean_space_gen: ``` lp15@70097 ` 1834` ``` assumes "n \ m" and U: "openin (Euclidean_space m) U" ``` lp15@70097 ` 1835` ``` and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f" ``` lp15@70097 ` 1836` ``` and "inj_on f U" ``` lp15@70097 ` 1837` ``` shows "openin (Euclidean_space n) (f ` U)" ``` lp15@70097 ` 1838` ```proof - ``` lp15@70097 ` 1839` ``` have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))" ``` lp15@70097 ` 1840` ``` by (metis Euclidean_space_def \n \ m\ inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space) ``` lp15@70097 ` 1841` ``` moreover have "U \ topspace (subtopology (Euclidean_space m) U)" ``` lp15@70097 ` 1842` ``` by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace) ``` lp15@70097 ` 1843` ``` ultimately show ?thesis ``` lp15@70097 ` 1844` ``` by (metis (no_types) U \inj_on f U\ cmf continuous_map_in_subtopology inf.absorb_iff2 ``` lp15@70097 ` 1845` ``` inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace) ``` lp15@70097 ` 1846` ```qed ``` lp15@70097 ` 1847` lp15@70097 ` 1848` ```corollary invariance_of_domain_Euclidean_space_embedding_map_gen: ``` lp15@70097 ` 1849` ``` assumes "n \ m" and U: "openin (Euclidean_space m) U" ``` lp15@70097 ` 1850` ``` and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f" ``` lp15@70097 ` 1851` ``` and "inj_on f U" ``` lp15@70097 ` 1852` ``` shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f" ``` lp15@70097 ` 1853` ``` proof (rule injective_open_imp_embedding_map [OF cmf]) ``` lp15@70097 ` 1854` ``` show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f" ``` lp15@70097 ` 1855` ``` by (meson U \n \ m\ \inj_on f U\ cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology subset_inj_on) ``` lp15@70097 ` 1856` ``` show "inj_on f (topspace (subtopology (Euclidean_space m) U))" ``` lp15@70097 ` 1857` ``` using assms openin_subset topspace_subtopology_subset by fastforce ``` lp15@70097 ` 1858` ```qed ``` lp15@70097 ` 1859` lp15@70097 ` 1860` lp15@70097 ` 1861` ```subsection\Relating two variants of Euclidean space, one within product topology. \ ``` lp15@70097 ` 1862` lp15@70097 ` 1863` ```proposition homeomorphic_maps_Euclidean_space_euclidean_gen_OLD: ``` lp15@70097 ` 1864` ``` fixes B :: "'n::euclidean_space set" ``` lp15@70097 ` 1865` ``` assumes "finite B" "independent B" and orth: "pairwise orthogonal B" and n: "card B = n" ``` lp15@70097 ` 1866` ``` obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g" ``` lp15@70097 ` 1867` ```proof - ``` lp15@70097 ` 1868` ``` note representation_basis [OF \independent B\, simp] ``` lp15@70097 ` 1869` ``` obtain b where injb: "inj_on b {..finite B\] ``` lp15@70097 ` 1871` ``` by (metis n card_Collect_less_nat card_image lessThan_def) ``` lp15@70097 ` 1872` ``` then have biB: "\i. i < n \ b i \ B" ``` lp15@70097 ` 1873` ``` by force ``` lp15@70097 ` 1874` ``` have repr: "\v. v \ span B \ (\iR b i) = v" ``` lp15@70097 ` 1875` ``` using real_vector.sum_representation_eq [OF \independent B\ _ \finite B\] ``` lp15@70097 ` 1876` ``` by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong) ``` lp15@70097 ` 1877` ``` let ?f = "\x. \iR b i" ``` lp15@70097 ` 1878` ``` let ?g = "\v i. if i < n then representation B v (b i) else 0" ``` lp15@70097 ` 1879` ``` show thesis ``` lp15@70097 ` 1880` ``` proof ``` lp15@70097 ` 1881` ``` show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) ?f ?g" ``` lp15@70097 ` 1882` ``` unfolding homeomorphic_maps_def ``` lp15@70097 ` 1883` ``` proof (intro conjI) ``` lp15@70097 ` 1884` ``` have *: "continuous_map euclidean (top_of_set (span B)) ?f" ``` lp15@70097 ` 1885` ``` by (metis (mono_tags) biB continuous_map_span_sum lessThan_iff) ``` lp15@70097 ` 1886` ``` show "continuous_map (Euclidean_space n) (top_of_set (span B)) ?f" ``` lp15@70097 ` 1887` ``` unfolding Euclidean_space_def ``` lp15@70097 ` 1888` ``` by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *) ``` lp15@70097 ` 1889` ``` show "continuous_map (top_of_set (span B)) (Euclidean_space n) ?g" ``` lp15@70097 ` 1890` ``` unfolding Euclidean_space_def ``` lp15@70097 ` 1891` ``` by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \independent B\ biB orth pairwise_orthogonal_imp_finite) ``` lp15@70097 ` 1892` ``` have [simp]: "\x i. i x i *\<^sub>R b i \ span B" ``` lp15@70097 ` 1893` ``` by (simp add: biB span_base span_scale) ``` lp15@70097 ` 1894` ``` have "representation B (?f x) (b j) = x j" ``` lp15@70097 ` 1895` ``` if 0: "\i\n. x i = (0::real)" and "j < n" for x j ``` lp15@70097 ` 1896` ``` proof - ``` lp15@70097 ` 1897` ``` have "representation B (?f x) (b j) = (\iR b i) (b j))" ``` lp15@70097 ` 1898` ``` by (subst real_vector.representation_sum) (auto simp add: \independent B\) ``` lp15@70097 ` 1899` ``` also have "... = (\iix\topspace (Euclidean_space n). ?g (?f x) = x" ``` lp15@70097 ` 1908` ``` by (auto simp: Euclidean_space_def) ``` lp15@70097 ` 1909` ``` show "\y\topspace (top_of_set (span B)). ?f (?g y) = y" ``` lp15@70097 ` 1910` ``` using repr by (auto simp: Euclidean_space_def) ``` lp15@70097 ` 1911` ``` qed ``` lp15@70097 ` 1912` ``` qed ``` lp15@70097 ` 1913` ```qed ``` lp15@70097 ` 1914` lp15@70097 ` 1915` ```proposition homeomorphic_maps_Euclidean_space_euclidean_gen: ``` lp15@70097 ` 1916` ``` fixes B :: "'n::euclidean_space set" ``` lp15@70097 ` 1917` ``` assumes "independent B" and orth: "pairwise orthogonal B" and n: "card B = n" ``` lp15@70097 ` 1918` ``` and 1: "\u. u \ B \ norm u = 1" ``` lp15@70097 ` 1919` ``` obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g" ``` lp15@70097 ` 1920` ``` and "\x. x \ topspace (Euclidean_space n) \ (norm (f x))\<^sup>2 = (\i2)" ``` lp15@70097 ` 1921` ```proof - ``` lp15@70097 ` 1922` ``` note representation_basis [OF \independent B\, simp] ``` lp15@70097 ` 1923` ``` have "finite B" ``` lp15@70097 ` 1924` ``` using \independent B\ finiteI_independent by metis ``` lp15@70097 ` 1925` ``` obtain b where injb: "inj_on b {..finite B\] ``` lp15@70097 ` 1927` ``` by (metis n card_Collect_less_nat card_image lessThan_def) ``` lp15@70097 ` 1928` ``` then have biB: "\i. i < n \ b i \ B" ``` lp15@70097 ` 1929` ``` by force ``` lp15@70097 ` 1930` ``` have "0 \ B" ``` lp15@70097 ` 1931` ``` using \independent B\ dependent_zero by blast ``` lp15@70097 ` 1932` ``` have [simp]: "b i \ b j = (if j = i then 1 else 0)" ``` lp15@70097 ` 1933` ``` if "i < n" "j < n" for i j ``` lp15@70097 ` 1934` ``` proof (cases "i = j") ``` lp15@70097 ` 1935` ``` case True ``` lp15@70097 ` 1936` ``` with 1 that show ?thesis ``` lp15@70097 ` 1937` ``` by (auto simp: norm_eq_sqrt_inner biB) ``` lp15@70097 ` 1938` ``` next ``` lp15@70097 ` 1939` ``` case False ``` lp15@70097 ` 1940` ``` then have "b i \ b j" ``` lp15@70097 ` 1941` ``` by (meson inj_onD injb lessThan_iff that) ``` lp15@70097 ` 1942` ``` then show ?thesis ``` lp15@70097 ` 1943` ``` using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB) ``` lp15@70097 ` 1944` ``` qed ``` lp15@70097 ` 1945` ``` have [simp]: "\x i. i x i *\<^sub>R b i \ span B" ``` lp15@70097 ` 1946` ``` by (simp add: biB span_base span_scale) ``` lp15@70097 ` 1947` ``` have repr: "\v. v \ span B \ (\iR b i) = v" ``` lp15@70097 ` 1948` ``` using real_vector.sum_representation_eq [OF \independent B\ _ \finite B\] ``` lp15@70097 ` 1949` ``` by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong) ``` lp15@70097 ` 1950` ``` define f where "f \ \x. \iR b i" ``` lp15@70097 ` 1951` ``` define g where "g \ \v i. if i < n then representation B v (b i) else 0" ``` lp15@70097 ` 1952` ``` show thesis ``` lp15@70097 ` 1953` ``` proof ``` lp15@70097 ` 1954` ``` show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g" ``` lp15@70097 ` 1955` ``` unfolding homeomorphic_maps_def ``` lp15@70097 ` 1956` ``` proof (intro conjI) ``` lp15@70097 ` 1957` ``` have *: "continuous_map euclidean (top_of_set (span B)) f" ``` lp15@70097 ` 1958` ``` unfolding f_def ``` lp15@70097 ` 1959` ``` by (rule continuous_map_span_sum) (use biB \0 \ B\ in auto) ``` lp15@70097 ` 1960` ``` show "continuous_map (Euclidean_space n) (top_of_set (span B)) f" ``` lp15@70097 ` 1961` ``` unfolding Euclidean_space_def ``` lp15@70097 ` 1962` ``` by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *) ``` lp15@70097 ` 1963` ``` show "continuous_map (top_of_set (span B)) (Euclidean_space n) g" ``` lp15@70097 ` 1964` ``` unfolding Euclidean_space_def g_def ``` lp15@70097 ` 1965` ``` by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \independent B\ biB orth pairwise_orthogonal_imp_finite) ``` lp15@70097 ` 1966` ``` have "representation B (f x) (b j) = x j" ``` lp15@70097 ` 1967` ``` if 0: "\i\n. x i = (0::real)" and "j < n" for x j ```