(* Author: John Harrison Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP *) (* At the moment this is just Brouwer's fixpoint theorem. The proof is from *) (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518 *) (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf". *) (* *) (* The script below is quite messy, but at least we avoid formalizing any *) (* topological machinery; we don't even use barycentric subdivision; this is *) (* the big advantage of Kuhn's proof over the usual Sperner's lemma one. *) (* *) (* (c) Copyright, John Harrison 1998-2008 *) section ‹Brouwer's Fixed Point Theorem› theory Brouwer_Fixpoint imports Path_Connected Homeomorphism Continuous_Extension begin subsection ‹Retractions› lemma retract_of_contractible: assumes "contractible T" "S retract_of T" shows "contractible S" using assms apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with) apply (rule_tac x="r a" in exI) apply (rule_tac x="r ∘ h" in exI) apply (intro conjI continuous_intros continuous_on_compose) apply (erule continuous_on_subset | force)+ done lemma retract_of_path_connected: "⟦path_connected T; S retract_of T⟧ ⟹ path_connected S" by (metis path_connected_continuous_image retract_of_def retraction) lemma retract_of_simply_connected: "⟦simply_connected T; S retract_of T⟧ ⟹ simply_connected S" apply (simp add: retract_of_def retraction_def, clarify) apply (rule simply_connected_retraction_gen) apply (force elim!: continuous_on_subset)+ done lemma retract_of_homotopically_trivial: assumes ts: "T retract_of S" and hom: "⋀f g. ⟦continuous_on U f; f ` U ⊆ S; continuous_on U g; g ` U ⊆ S⟧ ⟹ homotopic_with_canon (λx. True) U S f g" and "continuous_on U f" "f ` U ⊆ T" and "continuous_on U g" "g ` U ⊆ T" shows "homotopic_with_canon (λx. True) U T f g" proof - obtain r where "r ` S ⊆ S" "continuous_on S r" "∀x∈S. r (r x) = r x" "T = r ` S" using ts by (auto simp: retract_of_def retraction) then obtain k where "Retracts S r T k" unfolding Retracts_def by (metis continuous_on_subset dual_order.trans image_iff image_mono) then show ?thesis apply (rule Retracts.homotopically_trivial_retraction_gen) using assms apply (force simp: hom)+ done qed lemma retract_of_homotopically_trivial_null: assumes ts: "T retract_of S" and hom: "⋀f. ⟦continuous_on U f; f ` U ⊆ S⟧ ⟹ ∃c. homotopic_with_canon (λx. True) U S f (λx. c)" and "continuous_on U f" "f ` U ⊆ T" obtains c where "homotopic_with_canon (λx. True) U T f (λx. c)" proof - obtain r where "r ` S ⊆ S" "continuous_on S r" "∀x∈S. r (r x) = r x" "T = r ` S" using ts by (auto simp: retract_of_def retraction) then obtain k where "Retracts S r T k" unfolding Retracts_def by (metis continuous_on_subset dual_order.trans image_iff image_mono) then show ?thesis apply (rule Retracts.homotopically_trivial_retraction_null_gen) apply (rule TrueI refl assms that | assumption)+ done qed lemma retraction_openin_vimage_iff: "openin (top_of_set S) (S ∩ r -` U) ⟷ openin (top_of_set T) U" if retraction: "retraction S T r" and "U ⊆ T" using retraction apply (rule retractionE) apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) using ‹U ⊆ T› apply (auto elim: continuous_on_subset) done lemma retract_of_locally_compact: fixes S :: "'a :: {heine_borel,real_normed_vector} set" shows "⟦ locally compact S; T retract_of S⟧ ⟹ locally compact T" by (metis locally_compact_closedin closedin_retract) lemma homotopic_into_retract: "⟦f ` S ⊆ T; g ` S ⊆ T; T retract_of U; homotopic_with_canon (λx. True) S U f g⟧ ⟹ homotopic_with_canon (λx. True) S T f g" apply (subst (asm) homotopic_with_def) apply (simp add: homotopic_with retract_of_def retraction_def, clarify) apply (rule_tac x="r ∘ h" in exI) apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+ done lemma retract_of_locally_connected: assumes "locally connected T" "S retract_of T" shows "locally connected S" using assms by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE) lemma retract_of_locally_path_connected: assumes "locally path_connected T" "S retract_of T" shows "locally path_connected S" using assms by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE) text ‹A few simple lemmas about deformation retracts› lemma deformation_retract_imp_homotopy_eqv: fixes S :: "'a::euclidean_space set" assumes "homotopic_with_canon (λx. True) S S id r" and r: "retraction S T r" shows "S homotopy_eqv T" proof - have "homotopic_with_canon (λx. True) S S (id ∘ r) id" by (simp add: assms(1) homotopic_with_symD) moreover have "homotopic_with_canon (λx. True) T T (r ∘ id) id" using r unfolding retraction_def by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology) ultimately show ?thesis unfolding homotopy_equivalent_space_def by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def) qed lemma deformation_retract: fixes S :: "'a::euclidean_space set" shows "(∃r. homotopic_with_canon (λx. True) S S id r ∧ retraction S T r) ⟷ T retract_of S ∧ (∃f. homotopic_with_canon (λx. True) S S id f ∧ f ` S ⊆ T)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (auto simp: retract_of_def retraction_def) next assume ?rhs then show ?lhs apply (clarsimp simp add: retract_of_def retraction_def) apply (rule_tac x=r in exI, simp) apply (rule homotopic_with_trans, assumption) apply (rule_tac f = "r ∘ f" and g="r ∘ id" in homotopic_with_eq) apply (rule_tac Y=S in homotopic_compose_continuous_left) apply (auto simp: homotopic_with_sym) done qed lemma deformation_retract_of_contractible_sing: fixes S :: "'a::euclidean_space set" assumes "contractible S" "a ∈ S" obtains r where "homotopic_with_canon (λx. True) S S id r" "retraction S {a} r" proof - have "{a} retract_of S" by (simp add: ‹a ∈ S›) moreover have "homotopic_with_canon (λx. True) S S id (λx. a)" using assms by (auto simp: contractible_def homotopic_into_contractible image_subset_iff) moreover have "(λx. a) ` S ⊆ {a}" by (simp add: image_subsetI) ultimately show ?thesis using that deformation_retract by metis qed lemma continuous_on_compact_surface_projection_aux: fixes S :: "'a::t2_space set" assumes "compact S" "S ⊆ T" "image q T ⊆ S" and contp: "continuous_on T p" and "⋀x. x ∈ S ⟹ q x = x" and [simp]: "⋀x. x ∈ T ⟹ q(p x) = q x" and "⋀x. x ∈ T ⟹ p(q x) = p x" shows "continuous_on T q" proof - have *: "image p T = image p S" using assms by auto (metis imageI subset_iff) have contp': "continuous_on S p" by (rule continuous_on_subset [OF contp ‹S ⊆ T›]) have "continuous_on (p ` T) q" by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD) then have "continuous_on T (q ∘ p)" by (rule continuous_on_compose [OF contp]) then show ?thesis by (rule continuous_on_eq [of _ "q ∘ p"]) (simp add: o_def) qed lemma continuous_on_compact_surface_projection: fixes S :: "'a::real_normed_vector set" assumes "compact S" and S: "S ⊆ V - {0}" and "cone V" and iff: "⋀x k. x ∈ V - {0} ⟹ 0 < k ∧ (k *⇩_{R}x) ∈ S ⟷ d x = k" shows "continuous_on (V - {0}) (λx. d x *⇩_{R}x)" proof (rule continuous_on_compact_surface_projection_aux [OF ‹compact S› S]) show "(λx. d x *⇩_{R}x) ` (V - {0}) ⊆ S" using iff by auto show "continuous_on (V - {0}) (λx. inverse(norm x) *⇩_{R}x)" by (intro continuous_intros) force show "⋀x. x ∈ S ⟹ d x *⇩_{R}x = x" by (metis S zero_less_one local.iff scaleR_one subset_eq) show "d (x /⇩_{R}norm x) *⇩_{R}(x /⇩_{R}norm x) = d x *⇩_{R}x" if "x ∈ V - {0}" for x using iff [of "inverse(norm x) *⇩_{R}x" "norm x * d x", symmetric] iff that ‹cone V› by (simp add: field_simps cone_def zero_less_mult_iff) show "d x *⇩_{R}x /⇩_{R}norm (d x *⇩_{R}x) = x /⇩_{R}norm x" if "x ∈ V - {0}" for x proof - have "0 < d x" using local.iff that by blast then show ?thesis by simp qed qed subsection ‹Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts› text ‹Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding in spaces of higher dimension. John Harrison writes: "This turns out to be sufficient (since any set in ‹ℝ⇧^{n}› can be embedded as a closed subset of a convex subset of ‹ℝ⇧^{n}⇧^{+}⇧^{1}›) to derive the usual definitions, but we need to split them into two implications because of the lack of type quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."› definition✐‹tag important› AR :: "'a::topological_space set ⇒ bool" where "AR S ≡ ∀U. ∀S'::('a * real) set. S homeomorphic S' ∧ closedin (top_of_set U) S' ⟶ S' retract_of U" definition✐‹tag important› ANR :: "'a::topological_space set ⇒ bool" where "ANR S ≡ ∀U. ∀S'::('a * real) set. S homeomorphic S' ∧ closedin (top_of_set U) S' ⟶ (∃T. openin (top_of_set U) T ∧ S' retract_of T)" definition✐‹tag important› ENR :: "'a::topological_space set ⇒ bool" where "ENR S ≡ ∃U. open U ∧ S retract_of U" text ‹First, show that we do indeed get the "usual" properties of ARs and ANRs.› lemma AR_imp_absolute_extensor: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "AR S" and contf: "continuous_on T f" and "f ` T ⊆ S" and cloUT: "closedin (top_of_set U) T" obtains g where "continuous_on U g" "g ` U ⊆ S" "⋀x. x ∈ T ⟹ g x = f x" proof - have "aff_dim S < int (DIM('b × real))" using aff_dim_le_DIM [of S] by simp then obtain C and S' :: "('b * real) set" where C: "convex C" "C ≠ {}" and cloCS: "closedin (top_of_set C) S'" and hom: "S homeomorphic S'" by (metis that homeomorphic_closedin_convex) then have "S' retract_of C" using ‹AR S› by (simp add: AR_def) then obtain r where "S' ⊆ C" and contr: "continuous_on C r" and "r ` C ⊆ S'" and rid: "⋀x. x∈S' ⟹ r x = x" by (auto simp: retraction_def retract_of_def) obtain g h where "homeomorphism S S' g h" using hom by (force simp: homeomorphic_def) then have "continuous_on (f ` T) g" by (meson ‹f ` T ⊆ S› continuous_on_subset homeomorphism_def) then have contgf: "continuous_on T (g ∘ f)" by (metis continuous_on_compose contf) have gfTC: "(g ∘ f) ` T ⊆ C" proof - have "g ` S = S'" by (metis (no_types) ‹homeomorphism S S' g h› homeomorphism_def) with ‹S' ⊆ C› ‹f ` T ⊆ S› show ?thesis by force qed obtain f' where f': "continuous_on U f'" "f' ` U ⊆ C" "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x" by (metis Dugundji [OF C cloUT contgf gfTC]) show ?thesis proof (rule_tac g = "h ∘ r ∘ f'" in that) show "continuous_on U (h ∘ r ∘ f')" apply (intro continuous_on_compose f') using continuous_on_subset contr f' apply blast by (meson ‹homeomorphism S S' g h› ‹r ` C ⊆ S'› continuous_on_subset ‹f' ` U ⊆ C› homeomorphism_def image_mono) show "(h ∘ r ∘ f') ` U ⊆ S" using ‹homeomorphism S S' g h› ‹r ` C ⊆ S'› ‹f' ` U ⊆ C› by (fastforce simp: homeomorphism_def) show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x" using ‹homeomorphism S S' g h› ‹f ` T ⊆ S› f' by (auto simp: rid homeomorphism_def) qed qed lemma AR_imp_absolute_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "AR S" "S homeomorphic S'" and clo: "closedin (top_of_set U) S'" shows "S' retract_of U" proof - obtain g h where hom: "homeomorphism S S' g h" using assms by (force simp: homeomorphic_def) have h: "continuous_on S' h" " h ` S' ⊆ S" using hom homeomorphism_def apply blast apply (metis hom equalityE homeomorphism_def) done obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S" and h'h: "⋀x. x ∈ S' ⟹ h' x = h x" by (blast intro: AR_imp_absolute_extensor [OF ‹AR S› h clo]) have [simp]: "S' ⊆ U" using clo closedin_limpt by blast show ?thesis proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g ∘ h')" apply (intro continuous_on_compose h') apply (meson hom continuous_on_subset h' homeomorphism_cont1) done show "(g ∘ h') ` U ⊆ S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈S'. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed qed lemma AR_imp_absolute_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "AR S" and hom: "S homeomorphic S'" and clo: "closed S'" shows "S' retract_of UNIV" apply (rule AR_imp_absolute_retract [OF ‹AR S› hom]) using clo closed_closedin by auto lemma absolute_extensor_imp_AR: fixes S :: "'a::euclidean_space set" assumes "⋀f :: 'a * real ⇒ 'a. ⋀U T. ⟦continuous_on T f; f ` T ⊆ S; closedin (top_of_set U) T⟧ ⟹ ∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)" shows "AR S" proof (clarsimp simp: AR_def) fix U and T :: "('a * real) set" assume "S homeomorphic T" and clo: "closedin (top_of_set U) T" then obtain g h where hom: "homeomorphism S T g h" by (force simp: homeomorphic_def) have h: "continuous_on T h" " h ` T ⊆ S" using hom homeomorphism_def apply blast apply (metis hom equalityE homeomorphism_def) done obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S" and h'h: "∀x∈T. h' x = h x" using assms [OF h clo] by blast have [simp]: "T ⊆ U" using clo closedin_imp_subset by auto show "T retract_of U" proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g ∘ h')" apply (intro continuous_on_compose h') apply (meson hom continuous_on_subset h' homeomorphism_cont1) done show "(g ∘ h') ` U ⊆ T" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈T. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed qed lemma AR_eq_absolute_extensor: fixes S :: "'a::euclidean_space set" shows "AR S ⟷ (∀f :: 'a * real ⇒ 'a. ∀U T. continuous_on T f ⟶ f ` T ⊆ S ⟶ closedin (top_of_set U) T ⟶ (∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)))" apply (rule iffI) apply (metis AR_imp_absolute_extensor) apply (simp add: absolute_extensor_imp_AR) done lemma AR_imp_retract: fixes S :: "'a::euclidean_space set" assumes "AR S ∧ closedin (top_of_set U) S" shows "S retract_of U" using AR_imp_absolute_retract assms homeomorphic_refl by blast lemma AR_homeomorphic_AR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "AR T" "S homeomorphic T" shows "AR S" unfolding AR_def by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym) lemma homeomorphic_AR_iff_AR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" shows "S homeomorphic T ⟹ AR S ⟷ AR T" by (metis AR_homeomorphic_AR homeomorphic_sym) lemma ANR_imp_absolute_neighbourhood_extensor: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "ANR S" and contf: "continuous_on T f" and "f ` T ⊆ S" and cloUT: "closedin (top_of_set U) T" obtains V g where "T ⊆ V" "openin (top_of_set U) V" "continuous_on V g" "g ` V ⊆ S" "⋀x. x ∈ T ⟹ g x = f x" proof - have "aff_dim S < int (DIM('b × real))" using aff_dim_le_DIM [of S] by simp then obtain C and S' :: "('b * real) set" where C: "convex C" "C ≠ {}" and cloCS: "closedin (top_of_set C) S'" and hom: "S homeomorphic S'" by (metis that homeomorphic_closedin_convex) then obtain D where opD: "openin (top_of_set C) D" and "S' retract_of D" using ‹ANR S› by (auto simp: ANR_def) then obtain r where "S' ⊆ D" and contr: "continuous_on D r" and "r ` D ⊆ S'" and rid: "⋀x. x ∈ S' ⟹ r x = x" by (auto simp: retraction_def retract_of_def) obtain g h where homgh: "homeomorphism S S' g h" using hom by (force simp: homeomorphic_def) have "continuous_on (f ` T) g" by (meson ‹f ` T ⊆ S› continuous_on_subset homeomorphism_def homgh) then have contgf: "continuous_on T (g ∘ f)" by (intro continuous_on_compose contf) have gfTC: "(g ∘ f) ` T ⊆ C" proof - have "g ` S = S'" by (metis (no_types) homeomorphism_def homgh) then show ?thesis by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology) qed obtain f' where contf': "continuous_on U f'" and "f' ` U ⊆ C" and eq: "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x" by (metis Dugundji [OF C cloUT contgf gfTC]) show ?thesis proof (rule_tac V = "U ∩ f' -` D" and g = "h ∘ r ∘ f'" in that) show "T ⊆ U ∩ f' -` D" using cloUT closedin_imp_subset ‹S' ⊆ D› ‹f ` T ⊆ S› eq homeomorphism_image1 homgh by fastforce show ope: "openin (top_of_set U) (U ∩ f' -` D)" using ‹f' ` U ⊆ C› by (auto simp: opD contf' continuous_openin_preimage) have conth: "continuous_on (r ` f' ` (U ∩ f' -` D)) h" apply (rule continuous_on_subset [of S']) using homeomorphism_def homgh apply blast using ‹r ` D ⊆ S'› by blast show "continuous_on (U ∩ f' -` D) (h ∘ r ∘ f')" apply (intro continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto) done show "(h ∘ r ∘ f') ` (U ∩ f' -` D) ⊆ S" using ‹homeomorphism S S' g h› ‹f' ` U ⊆ C› ‹r ` D ⊆ S'› by (auto simp: homeomorphism_def) show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x" using ‹homeomorphism S S' g h› ‹f ` T ⊆ S› eq by (auto simp: rid homeomorphism_def) qed qed corollary ANR_imp_absolute_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" "S homeomorphic S'" and clo: "closedin (top_of_set U) S'" obtains V where "openin (top_of_set U) V" "S' retract_of V" proof - obtain g h where hom: "homeomorphism S S' g h" using assms by (force simp: homeomorphic_def) have h: "continuous_on S' h" " h ` S' ⊆ S" using hom homeomorphism_def apply blast apply (metis hom equalityE homeomorphism_def) done from ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo] obtain V h' where "S' ⊆ V" and opUV: "openin (top_of_set U) V" and h': "continuous_on V h'" "h' ` V ⊆ S" and h'h:"⋀x. x ∈ S' ⟹ h' x = h x" by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo]) have "S' retract_of V" proof (simp add: retraction_def retract_of_def, intro exI conjI ‹S' ⊆ V›) show "continuous_on V (g ∘ h')" apply (intro continuous_on_compose h') apply (meson hom continuous_on_subset h' homeomorphism_cont1) done show "(g ∘ h') ` V ⊆ S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈S'. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed then show ?thesis by (rule that [OF opUV]) qed corollary ANR_imp_absolute_neighbourhood_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'" obtains V where "open V" "S' retract_of V" using ANR_imp_absolute_neighbourhood_retract [OF ‹ANR S› hom] by (metis clo closed_closedin open_openin subtopology_UNIV) corollary neighbourhood_extension_into_ANR: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and fim: "f ` S ⊆ T" and "ANR T" "closed S" obtains V g where "S ⊆ V" "open V" "continuous_on V g" "g ` V ⊆ T" "⋀x. x ∈ S ⟹ g x = f x" using ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf fim] by (metis ‹closed S› closed_closedin open_openin subtopology_UNIV) lemma absolute_neighbourhood_extensor_imp_ANR: fixes S :: "'a::euclidean_space set" assumes "⋀f :: 'a * real ⇒ 'a. ⋀U T. ⟦continuous_on T f; f ` T ⊆ S; closedin (top_of_set U) T⟧ ⟹ ∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ` V ⊆ S ∧ (∀x ∈ T. g x = f x)" shows "ANR S" proof (clarsimp simp: ANR_def) fix U and T :: "('a * real) set" assume "S homeomorphic T" and clo: "closedin (top_of_set U) T" then obtain g h where hom: "homeomorphism S T g h" by (force simp: homeomorphic_def) have h: "continuous_on T h" " h ` T ⊆ S" using hom homeomorphism_def apply blast apply (metis hom equalityE homeomorphism_def) done obtain V h' where "T ⊆ V" and opV: "openin (top_of_set U) V" and h': "continuous_on V h'" "h' ` V ⊆ S" and h'h: "∀x∈T. h' x = h x" using assms [OF h clo] by blast have [simp]: "T ⊆ U" using clo closedin_imp_subset by auto have "T retract_of V" proof (simp add: retraction_def retract_of_def, intro exI conjI ‹T ⊆ V›) show "continuous_on V (g ∘ h')" apply (intro continuous_on_compose h') apply (meson hom continuous_on_subset h' homeomorphism_cont1) done show "(g ∘ h') ` V ⊆ T" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈T. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed then show "∃V. openin (top_of_set U) V ∧ T retract_of V" using opV by blast qed lemma ANR_eq_absolute_neighbourhood_extensor: fixes S :: "'a::euclidean_space set" shows "ANR S ⟷ (∀f :: 'a * real ⇒ 'a. ∀U T. continuous_on T f ⟶ f ` T ⊆ S ⟶ closedin (top_of_set U) T ⟶ (∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ` V ⊆ S ∧ (∀x ∈ T. g x = f x)))" apply (rule iffI) apply (metis ANR_imp_absolute_neighbourhood_extensor) apply (simp add: absolute_neighbourhood_extensor_imp_ANR) done lemma ANR_imp_neighbourhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR S" "closedin (top_of_set U) S" obtains V where "openin (top_of_set U) V" "S retract_of V" using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast lemma ANR_imp_absolute_closed_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" "S homeomorphic S'" and US': "closedin (top_of_set U) S'" obtains V W where "openin (top_of_set U) V" "closedin (top_of_set U) W" "S' ⊆ V" "V ⊆ W" "S' retract_of W" proof - obtain Z where "openin (top_of_set U) Z" and S'Z: "S' retract_of Z" by (blast intro: assms ANR_imp_absolute_neighbourhood_retract) then have UUZ: "closedin (top_of_set U) (U - Z)" by auto have "S' ∩ (U - Z) = {}" using ‹S' retract_of Z› closedin_retract closedin_subtopology by fastforce then obtain V W where "openin (top_of_set U) V" and "openin (top_of_set U) W" and "S' ⊆ V" "U - Z ⊆ W" "V ∩ W = {}" using separation_normal_local [OF US' UUZ] by auto moreover have "S' retract_of U - W" apply (rule retract_of_subset [OF S'Z]) using US' ‹S' ⊆ V› ‹V ∩ W = {}› closedin_subset apply fastforce using Diff_subset_conv ‹U - Z ⊆ W› by blast ultimately show ?thesis apply (rule_tac V=V and W = "U-W" in that) using openin_imp_subset apply force+ done qed lemma ANR_imp_closed_neighbourhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR S" "closedin (top_of_set U) S" obtains V W where "openin (top_of_set U) V" "closedin (top_of_set U) W" "S ⊆ V" "V ⊆ W" "S retract_of W" by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl) lemma ANR_homeomorphic_ANR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ANR T" "S homeomorphic T" shows "ANR S" unfolding ANR_def by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym) lemma homeomorphic_ANR_iff_ANR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" shows "S homeomorphic T ⟹ ANR S ⟷ ANR T" by (metis ANR_homeomorphic_ANR homeomorphic_sym) subsubsection ‹Analogous properties of ENRs› lemma ENR_imp_absolute_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ENR S" and hom: "S homeomorphic S'" and "S' ⊆ U" obtains V where "openin (top_of_set U) V" "S' retract_of V" proof - obtain X where "open X" "S retract_of X" using ‹ENR S› by (auto simp: ENR_def) then obtain r where "retraction X S r" by (auto simp: retract_of_def) have "locally compact S'" using retract_of_locally_compact open_imp_locally_compact homeomorphic_local_compactness ‹S retract_of X› ‹open X› hom by blast then obtain W where UW: "openin (top_of_set U) W" and WS': "closedin (top_of_set W) S'" apply (rule locally_compact_closedin_open) apply (rename_tac W) apply (rule_tac W = "U ∩ W" in that, blast) by (simp add: ‹S' ⊆ U› closedin_limpt) obtain f g where hom: "homeomorphism S S' f g" using assms by (force simp: homeomorphic_def) have contg: "continuous_on S' g" using hom homeomorphism_def by blast moreover have "g ` S' ⊆ S" by (metis hom equalityE homeomorphism_def) ultimately obtain h where conth: "continuous_on W h" and hg: "⋀x. x ∈ S' ⟹ h x = g x" using Tietze_unbounded [of S' g W] WS' by blast have "W ⊆ U" using UW openin_open by auto have "S' ⊆ W" using WS' closedin_closed by auto have him: "⋀x. x ∈ S' ⟹ h x ∈ X" by (metis (no_types) ‹S retract_of X› hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq) have "S' retract_of (W ∩ h -` X)" proof (simp add: retraction_def retract_of_def, intro exI conjI) show "S' ⊆ W" "S' ⊆ h -` X" using him WS' closedin_imp_subset by blast+ show "continuous_on (W ∩ h -` X) (f ∘ r ∘ h)" proof (intro continuous_on_compose) show "continuous_on (W ∩ h -` X) h" by (meson conth continuous_on_subset inf_le1) show "continuous_on (h ` (W ∩ h -` X)) r" proof - have "h ` (W ∩ h -` X) ⊆ X" by blast then show "continuous_on (h ` (W ∩ h -` X)) r" by (meson ‹retraction X S r› continuous_on_subset retraction) qed show "continuous_on (r ` h ` (W ∩ h -` X)) f" apply (rule continuous_on_subset [of S]) using hom homeomorphism_def apply blast apply clarify apply (meson ‹retraction X S r› subsetD imageI retraction_def) done qed show "(f ∘ r ∘ h) ` (W ∩ h -` X) ⊆ S'" using ‹retraction X S r› hom by (auto simp: retraction_def homeomorphism_def) show "∀x∈S'. (f ∘ r ∘ h) x = x" using ‹retraction X S r› hom by (auto simp: retraction_def homeomorphism_def hg) qed then show ?thesis apply (rule_tac V = "W ∩ h -` X" in that) apply (rule openin_trans [OF _ UW]) using ‹continuous_on W h› ‹open X› continuous_openin_preimage_eq apply blast+ done qed corollary ENR_imp_absolute_neighbourhood_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ENR S" "S homeomorphic S'" obtains T' where "open T'" "S' retract_of T'" by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV) lemma ENR_homeomorphic_ENR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ENR T" "S homeomorphic T" shows "ENR S" unfolding ENR_def by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym) lemma homeomorphic_ENR_iff_ENR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" shows "ENR S ⟷ ENR T" by (meson ENR_homeomorphic_ENR assms homeomorphic_sym) lemma ENR_translation: fixes S :: "'a::euclidean_space set" shows "ENR(image (λx. a + x) S) ⟷ ENR S" by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR) lemma ENR_linear_image_eq: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "linear f" "inj f" shows "ENR (image f S) ⟷ ENR S" apply (rule homeomorphic_ENR_iff_ENR) using assms homeomorphic_sym linear_homeomorphic_image by auto text ‹Some relations among the concepts. We also relate AR to being a retract of UNIV, which is often a more convenient proxy in the closed case.› lemma AR_imp_ANR: "AR S ⟹ ANR S" using ANR_def AR_def by fastforce lemma ENR_imp_ANR: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ANR S" apply (simp add: ANR_def) by (metis ENR_imp_absolute_neighbourhood_retract closedin_imp_subset) lemma ENR_ANR: fixes S :: "'a::euclidean_space set" shows "ENR S ⟷ ANR S ∧ locally compact S" proof assume "ENR S" then have "locally compact S" using ENR_def open_imp_locally_compact retract_of_locally_compact by auto then show "ANR S ∧ locally compact S" using ENR_imp_ANR ‹ENR S› by blast next assume "ANR S ∧ locally compact S" then have "ANR S" "locally compact S" by auto then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T" using locally_compact_homeomorphic_closed by (metis DIM_prod DIM_real Suc_eq_plus1 lessI) then show "ENR S" using ‹ANR S› apply (simp add: ANR_def) apply (drule_tac x=UNIV in spec) apply (drule_tac x=T in spec, clarsimp) apply (meson ENR_def ENR_homeomorphic_ENR open_openin) done qed lemma AR_ANR: fixes S :: "'a::euclidean_space set" shows "AR S ⟷ ANR S ∧ contractible S ∧ S ≠ {}" (is "?lhs = ?rhs") proof assume ?lhs obtain C and S' :: "('a * real) set" where "convex C" "C ≠ {}" "closedin (top_of_set C) S'" "S homeomorphic S'" apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"]) using aff_dim_le_DIM [of S] by auto with ‹AR S› have "contractible S" apply (simp add: AR_def) apply (drule_tac x=C in spec) apply (drule_tac x="S'" in spec, simp) using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce with ‹AR S› show ?rhs apply (auto simp: AR_imp_ANR) apply (force simp: AR_def) done next assume ?rhs then obtain a and h:: "real × 'a ⇒ 'a" where conth: "continuous_on ({0..1} × S) h" and hS: "h ` ({0..1} × S) ⊆ S" and [simp]: "⋀x. h(0, x) = x" and [simp]: "⋀x. h(1, x) = a" and "ANR S" "S ≠ {}" by (auto simp: contractible_def homotopic_with_def) then have "a ∈ S" by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one) have "∃g. continuous_on W g ∧ g ` W ⊆ S ∧ (∀x∈T. g x = f x)" if f: "continuous_on T f" "f ` T ⊆ S" and WT: "closedin (top_of_set W) T" for W T and f :: "'a × real ⇒ 'a" proof - obtain U g where "T ⊆ U" and WU: "openin (top_of_set W) U" and contg: "continuous_on U g" and "g ` U ⊆ S" and gf: "⋀x. x ∈ T ⟹ g x = f x" using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor ‹ANR S›, rule_format, OF f WT] by auto have WWU: "closedin (top_of_set W) (W - U)" using WU closedin_diff by fastforce moreover have "(W - U) ∩ T = {}" using ‹T ⊆ U› by auto ultimately obtain V V' where WV': "openin (top_of_set W) V'" and WV: "openin (top_of_set W) V" and "W - U ⊆ V'" "T ⊆ V" "V' ∩ V = {}" using separation_normal_local [of W "W-U" T] WT by blast then have WVT: "T ∩ (W - V) = {}" by auto have WWV: "closedin (top_of_set W) (W - V)" using WV closedin_diff by fastforce obtain j :: " 'a × real ⇒ real" where contj: "continuous_on W j" and j: "⋀x. x ∈ W ⟹ j x ∈ {0..1}" and j0: "⋀x. x ∈ W - V ⟹ j x = 1" and j1: "⋀x. x ∈ T ⟹ j x = 0" by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment) have Weq: "W = (W - V) ∪ (W - V')" using ‹V' ∩ V = {}› by force show ?thesis proof (intro conjI exI) have *: "continuous_on (W - V') (λx. h (j x, g x))" apply (rule continuous_on_compose2 [OF conth continuous_on_Pair]) apply (rule continuous_on_subset [OF contj Diff_subset]) apply (rule continuous_on_subset [OF contg]) apply (metis Diff_subset_conv Un_commute ‹W - U ⊆ V'›) using j ‹g ` U ⊆ S› ‹W - U ⊆ V'› apply fastforce done show "continuous_on W (λx. if x ∈ W - V then a else h (j x, g x))" apply (subst Weq) apply (rule continuous_on_cases_local) apply (simp_all add: Weq [symmetric] WWV continuous_on_const *) using WV' closedin_diff apply fastforce apply (auto simp: j0 j1) done next have "h (j (x, y), g (x, y)) ∈ S" if "(x, y) ∈ W" "(x, y) ∈ V" for x y proof - have "j(x, y) ∈ {0..1}" using j that by blast moreover have "g(x, y) ∈ S" using ‹V' ∩ V = {}› ‹W - U ⊆ V'› ‹g ` U ⊆ S› that by fastforce ultimately show ?thesis using hS by blast qed with ‹a ∈ S› ‹g ` U ⊆ S› show "(λx. if x ∈ W - V then a else h (j x, g x)) ` W ⊆ S" by auto next show "∀x∈T. (if x ∈ W - V then a else h (j x, g x)) = f x" using ‹T ⊆ V› by (auto simp: j0 j1 gf) qed qed then show ?lhs by (simp add: AR_eq_absolute_extensor) qed lemma ANR_retract_of_ANR: fixes S :: "'a::euclidean_space set" assumes "ANR T" "S retract_of T" shows "ANR S" using assms apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def) apply (clarsimp elim!: all_forward) apply (erule impCE, metis subset_trans) apply (clarsimp elim!: ex_forward) apply (rule_tac x="r ∘ g" in exI) by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans) lemma AR_retract_of_AR: fixes S :: "'a::euclidean_space set" shows "⟦AR T; S retract_of T⟧ ⟹ AR S" using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce lemma ENR_retract_of_ENR: "⟦ENR T; S retract_of T⟧ ⟹ ENR S" by (meson ENR_def retract_of_trans) lemma retract_of_UNIV: fixes S :: "'a::euclidean_space set" shows "S retract_of UNIV ⟷ AR S ∧ closed S" by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV) lemma compact_AR: fixes S :: "'a::euclidean_space set" shows "compact S ∧ AR S ⟷ compact S ∧ S retract_of UNIV" using compact_imp_closed retract_of_UNIV by blast text ‹More properties of ARs, ANRs and ENRs› lemma not_AR_empty [simp]: "¬ AR({})" by (auto simp: AR_def) lemma ENR_empty [simp]: "ENR {}" by (simp add: ENR_def) lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)" by (simp add: ENR_imp_ANR) lemma convex_imp_AR: fixes S :: "'a::euclidean_space set" shows "⟦convex S; S ≠ {}⟧ ⟹ AR S" apply (rule absolute_extensor_imp_AR) apply (rule Dugundji, assumption+) by blast lemma convex_imp_ANR: fixes S :: "'a::euclidean_space set" shows "convex S ⟹ ANR S" using ANR_empty AR_imp_ANR convex_imp_AR by blast lemma ENR_convex_closed: fixes S :: "'a::euclidean_space set" shows "⟦closed S; convex S⟧ ⟹ ENR S" using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)" using retract_of_UNIV by auto lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)" by (simp add: AR_imp_ANR) lemma ENR_UNIV [simp]:"ENR UNIV" using ENR_def by blast lemma AR_singleton: fixes a :: "'a::euclidean_space" shows "AR {a}" using retract_of_UNIV by blast lemma ANR_singleton: fixes a :: "'a::euclidean_space" shows "ANR {a}" by (simp add: AR_imp_ANR AR_singleton) lemma ENR_singleton: "ENR {a}" using ENR_def by blast text ‹ARs closed under union› lemma AR_closed_Un_local_aux: fixes U :: "'a::euclidean_space set" assumes "closedin (top_of_set U) S" "closedin (top_of_set U) T" "AR S" "AR T" "AR(S ∩ T)" shows "(S ∪ T) retract_of U" proof - have "S ∩ T ≠ {}" using assms AR_def by fastforce have "S ⊆ U" "T ⊆ U" using assms by (auto simp: closedin_imp_subset) define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}" define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}" define W where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}" have US': "closedin (top_of_set U) S'" using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"] by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have UT': "closedin (top_of_set U) T'" using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"] by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have "S ⊆ S'" using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce have "T ⊆ T'" using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce have "S ∩ T ⊆ W" "W ⊆ U" using ‹S ⊆ U› by (auto simp: W_def setdist_sing_in_set) have "(S ∩ T) retract_of W" apply (rule AR_imp_absolute_retract [OF ‹AR(S ∩ T)›]) apply (simp add: homeomorphic_refl) apply (rule closedin_subset_trans [of U]) apply (simp_all add: assms closedin_Int ‹S ∩ T ⊆ W› ‹W ⊆ U›) done then obtain r0 where "S ∩ T ⊆ W" and contr0: "continuous_on W r0" and "r0 ` W ⊆ S ∩ T" and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x" by (auto simp: retract_of_def retraction_def) have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x using setdist_eq_0_closedin ‹S ∩ T ≠ {}› assms by (force simp: W_def setdist_sing_in_set) have "S' ∩ T' = W" by (auto simp: S'_def T'_def W_def) then have cloUW: "closedin (top_of_set U) W" using closedin_Int US' UT' by blast define r where "r ≡ λx. if x ∈ W then r0 x else x" have "r ` (W ∪ S) ⊆ S" "r ` (W ∪ T) ⊆ T" using ‹r0 ` W ⊆ S ∩ T› r_def by auto have contr: "continuous_on (W ∪ (S ∪ T)) r" unfolding r_def proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id]) show "closedin (top_of_set (W ∪ (S ∪ T))) W" using ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› ‹closedin (top_of_set U) W› closedin_subset_trans by fastforce show "closedin (top_of_set (W ∪ (S ∪ T))) (S ∪ T)" by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2) show "⋀x. x ∈ W ∧ x ∉ W ∨ x ∈ S ∪ T ∧ x ∈ W ⟹ r0 x = x" by (auto simp: ST) qed have cloUWS: "closedin (top_of_set U) (W ∪ S)" by (simp add: cloUW assms closedin_Un) obtain g where contg: "continuous_on U g" and "g ` U ⊆ S" and geqr: "⋀x. x ∈ W ∪ S ⟹ g x = r x" apply (rule AR_imp_absolute_extensor [OF ‹AR S› _ _ cloUWS]) apply (rule continuous_on_subset [OF contr]) using ‹r ` (W ∪ S) ⊆ S› apply auto done have cloUWT: "closedin (top_of_set U) (W ∪ T)" by (simp add: cloUW assms closedin_Un) obtain h where conth: "continuous_on U h" and "h ` U ⊆ T" and heqr: "⋀x. x ∈ W ∪ T ⟹ h x = r x" apply (rule AR_imp_absolute_extensor [OF ‹AR T› _ _ cloUWT]) apply (rule continuous_on_subset [OF contr]) using ‹r ` (W ∪ T) ⊆ T› apply auto done have "U = S' ∪ T'" by (force simp: S'_def T'_def) then have cont: "continuous_on U (λx. if x ∈ S' then g x else h x)" apply (rule ssubst) apply (rule continuous_on_cases_local) using US' UT' ‹S' ∩ T' = W› ‹U = S' ∪ T'› contg conth continuous_on_subset geqr heqr apply auto done have UST: "(λx. if x ∈ S' then g x else h x) ` U ⊆ S ∪ T" using ‹g ` U ⊆ S› ‹h ` U ⊆ T› by auto show ?thesis apply (simp add: retract_of_def retraction_def ‹S ⊆ U› ‹T ⊆ U›) apply (rule_tac x="λx. if x ∈ S' then g x else h x" in exI) apply (intro conjI cont UST) by (metis IntI ST Un_iff ‹S ⊆ S'› ‹S' ∩ T' = W› ‹T ⊆ T'› subsetD geqr heqr r0 r_def) qed lemma AR_closed_Un_local: fixes S :: "'a::euclidean_space set" assumes STS: "closedin (top_of_set (S ∪ T)) S" and STT: "closedin (top_of_set (S ∪ T)) T" and "AR S" "AR T" "AR(S ∩ T)" shows "AR(S ∪ T)" proof - have "C retract_of U" if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C" for U and C :: "('a * real) set" proof - obtain f g where hom: "homeomorphism (S ∪ T) C f g" using hom by (force simp: homeomorphic_def) have US: "closedin (top_of_set U) (C ∩ g -` S)" apply (rule closedin_trans [OF _ UC]) apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) using hom homeomorphism_def apply blast apply (metis hom homeomorphism_def set_eq_subset) done have UT: "closedin (top_of_set U) (C ∩ g -` T)" apply (rule closedin_trans [OF _ UC]) apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) using hom homeomorphism_def apply blast apply (metis hom homeomorphism_def set_eq_subset) done have ARS: "AR (C ∩ g -` S)" apply (rule AR_homeomorphic_AR [OF ‹AR S›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have ART: "AR (C ∩ g -` T)" apply (rule AR_homeomorphic_AR [OF ‹AR T›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have ARI: "AR ((C ∩ g -` S) ∩ (C ∩ g -` T))" apply (rule AR_homeomorphic_AR [OF ‹AR (S ∩ T)›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)" using hom by (auto simp: homeomorphism_def) then show ?thesis by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI]) qed then show ?thesis by (force simp: AR_def) qed corollary AR_closed_Un: fixes S :: "'a::euclidean_space set" shows "⟦closed S; closed T; AR S; AR T; AR (S ∩ T)⟧ ⟹ AR (S ∪ T)" by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV) text ‹ANRs closed under union› lemma ANR_closed_Un_local_aux: fixes U :: "'a::euclidean_space set" assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "ANR S" "ANR T" "ANR(S ∩ T)" obtains V where "openin (top_of_set U) V" "(S ∪ T) retract_of V" proof (cases "S = {} ∨ T = {}") case True with assms that show ?thesis by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb) next case False then have [simp]: "S ≠ {}" "T ≠ {}" by auto have "S ⊆ U" "T ⊆ U" using assms by (auto simp: closedin_imp_subset) define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}" define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}" define W where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}" have cloUS': "closedin (top_of_set U) S'" using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"] by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have cloUT': "closedin (top_of_set U) T'" using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"] by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have "S ⊆ S'" using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce have "T ⊆ T'" using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce have "S' ∪ T' = U" by (auto simp: S'_def T'_def) have "W ⊆ S'" by (simp add: Collect_mono S'_def W_def) have "W ⊆ T'" by (simp add: Collect_mono T'_def W_def) have ST_W: "S ∩ T ⊆ W" and "W ⊆ U" using ‹S ⊆ U› by (force simp: W_def setdist_sing_in_set)+ have "S' ∩ T' = W" by (auto simp: S'_def T'_def W_def) then have cloUW: "closedin (top_of_set U) W" using closedin_Int cloUS' cloUT' by blast obtain W' W0 where "openin (top_of_set W) W'" and cloWW0: "closedin (top_of_set W) W0" and "S ∩ T ⊆ W'" "W' ⊆ W0" and ret: "(S ∩ T) retract_of W0" apply (rule ANR_imp_closed_neighbourhood_retract [OF ‹ANR(S ∩ T)›]) apply (rule closedin_subset_trans [of U, OF _ ST_W ‹W ⊆ U›]) apply (blast intro: assms)+ done then obtain U0 where opeUU0: "openin (top_of_set U) U0" and U0: "S ∩ T ⊆ U0" "U0 ∩ W ⊆ W0" unfolding openin_open using ‹W ⊆ U› by blast have "W0 ⊆ U" using ‹W ⊆ U› cloWW0 closedin_subset by fastforce obtain r0 where "S ∩ T ⊆ W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 ⊆ S ∩ T" and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x" using ret by (force simp: retract_of_def retraction_def) have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin) define r where "r ≡ λx. if x ∈ W0 then r0 x else x" have "r ` (W0 ∪ S) ⊆ S" "r ` (W0 ∪ T) ⊆ T" using ‹r0 ` W0 ⊆ S ∩ T› r_def by auto have contr: "continuous_on (W0 ∪ (S ∪ T)) r" unfolding r_def proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id]) show "closedin (top_of_set (W0 ∪ (S ∪ T))) W0" apply (rule closedin_subset_trans [of U]) using cloWW0 cloUW closedin_trans ‹W0 ⊆ U› ‹S ⊆ U› ‹T ⊆ U› apply blast+ done show "closedin (top_of_set (W0 ∪ (S ∪ T))) (S ∪ T)" by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W0 ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2) show "⋀x. x ∈ W0 ∧ x ∉ W0 ∨ x ∈ S ∪ T ∧ x ∈ W0 ⟹ r0 x = x" using ST cloWW0 closedin_subset by fastforce qed have cloS'WS: "closedin (top_of_set S') (W0 ∪ S)" by (meson closedin_subset_trans US cloUS' ‹S ⊆ S'› ‹W ⊆ S'› cloUW cloWW0 closedin_Un closedin_imp_subset closedin_trans) obtain W1 g where "W0 ∪ S ⊆ W1" and contg: "continuous_on W1 g" and opeSW1: "openin (top_of_set S') W1" and "g ` W1 ⊆ S" and geqr: "⋀x. x ∈ W0 ∪ S ⟹ g x = r x" apply (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› _ ‹r ` (W0 ∪ S) ⊆ S› cloS'WS]) apply (rule continuous_on_subset [OF contr], blast+) done have cloT'WT: "closedin (top_of_set T') (W0 ∪ T)" by (meson closedin_subset_trans UT cloUT' ‹T ⊆ T'› ‹W ⊆ T'› cloUW cloWW0 closedin_Un closedin_imp_subset closedin_trans) obtain W2 h where "W0 ∪ T ⊆ W2" and conth: "continuous_on W2 h" and opeSW2: "openin (top_of_set T') W2" and "h ` W2 ⊆ T" and heqr: "⋀x. x ∈ W0 ∪ T ⟹ h x = r x" apply (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› _ ‹r ` (W0 ∪ T) ⊆ T› cloT'WT]) apply (rule continuous_on_subset [OF contr], blast+) done have "S' ∩ T' = W" by (force simp: S'_def T'_def W_def) obtain O1 O2 where "open O1" "W1 = S' ∩ O1" "open O2" "W2 = T' ∩ O2" using opeSW1 opeSW2 by (force simp: openin_open) show ?thesis proof have eq: "W1 - (W - U0) ∪ (W2 - (W - U0)) = ((U - T') ∩ O1 ∪ (U - S') ∩ O2 ∪ U ∩ O1 ∩ O2) - (W - U0)" using ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› by (auto simp: ‹S' ∪ T' = U› [symmetric] ‹S' ∩ T' = W› [symmetric] ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2›) show "openin (top_of_set U) (W1 - (W - U0) ∪ (W2 - (W - U0)))" apply (subst eq) apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' ‹open O1› ‹open O2›, simp_all) done have cloW1: "closedin (top_of_set (W1 - (W - U0) ∪ (W2 - (W - U0)))) (W1 - (W - U0))" using cloUS' apply (simp add: closedin_closed) apply (erule ex_forward) using U0 ‹W0 ∪ S ⊆ W1› apply (auto simp: ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2› ‹S' ∪ T' = U› [symmetric]‹S' ∩ T' = W› [symmetric]) done have cloW2: "closedin (top_of_set (W1 - (W - U0) ∪ (W2 - (W - U0)))) (W2 - (W - U0))" using cloUT' apply (simp add: closedin_closed) apply (erule ex_forward) using U0 ‹W0 ∪ T ⊆ W2› apply (auto simp: ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2› ‹S' ∪ T' = U› [symmetric]‹S' ∩ T' = W› [symmetric]) done have *: "∀x∈S ∪ T. (if x ∈ S' then g x else h x) = x" using ST ‹S' ∩ T' = W› cloT'WT closedin_subset geqr heqr apply (auto simp: r_def, fastforce) using ‹S ⊆ S'› ‹T ⊆ T'› ‹W0 ∪ S ⊆ W1› ‹W1 = S' ∩ O1› by auto have "∃r. continuous_on (W1 - (W - U0) ∪ (W2 - (W - U0))) r ∧ r ` (W1 - (W - U0) ∪ (W2 - (W - U0))) ⊆ S ∪ T ∧ (∀x∈S ∪ T. r x = x)" apply (rule_tac x = "λx. if x ∈ S' then g x else h x" in exI) apply (intro conjI *) apply (rule continuous_on_cases_local [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]]) using ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2› ‹S' ∩ T' = W› ‹g ` W1 ⊆ S› ‹h ` W2 ⊆ T› apply auto using ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1› apply (fastforce simp add: geqr heqr)+ done then show "S ∪ T retract_of W1 - (W - U0) ∪ (W2 - (W - U0))" using ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› ST opeUU0 U0 by (auto simp: retract_of_def retraction_def) qed qed lemma ANR_closed_Un_local: fixes S :: "'a::euclidean_space set" assumes STS: "closedin (top_of_set (S ∪ T)) S" and STT: "closedin (top_of_set (S ∪ T)) T" and "ANR S" "ANR T" "ANR(S ∩ T)" shows "ANR(S ∪ T)" proof - have "∃T. openin (top_of_set U) T ∧ C retract_of T" if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C" for U and C :: "('a * real) set" proof - obtain f g where hom: "homeomorphism (S ∪ T) C f g" using hom by (force simp: homeomorphic_def) have US: "closedin (top_of_set U) (C ∩ g -` S)" apply (rule closedin_trans [OF _ UC]) apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) using hom [unfolded homeomorphism_def] apply blast apply (metis hom homeomorphism_def set_eq_subset) done have UT: "closedin (top_of_set U) (C ∩ g -` T)" apply (rule closedin_trans [OF _ UC]) apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) using hom [unfolded homeomorphism_def] apply blast apply (metis hom homeomorphism_def set_eq_subset) done have ANRS: "ANR (C ∩ g -` S)" apply (rule ANR_homeomorphic_ANR [OF ‹ANR S›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have ANRT: "ANR (C ∩ g -` T)" apply (rule ANR_homeomorphic_ANR [OF ‹ANR T›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have ANRI: "ANR ((C ∩ g -` S) ∩ (C ∩ g -` T))" apply (rule ANR_homeomorphic_ANR [OF ‹ANR (S ∩ T)›]) apply (simp add: homeomorphic_def) apply (rule_tac x=g in exI) apply (rule_tac x=f in exI) using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)" using hom by (auto simp: homeomorphism_def) then show ?thesis by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI]) qed then show ?thesis by (auto simp: ANR_def) qed corollary ANR_closed_Un: fixes S :: "'a::euclidean_space set" shows "⟦closed S; closed T; ANR S; ANR T; ANR (S ∩ T)⟧ ⟹ ANR (S ∪ T)" by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int) lemma ANR_openin: fixes S :: "'a::euclidean_space set" assumes "ANR T" and opeTS: "openin (top_of_set T) S" shows "ANR S" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: "'a × real ⇒ 'a" and U C assume contf: "continuous_on C f" and fim: "f ` C ⊆ S" and cloUC: "closedin (top_of_set U) C" have "f ` C ⊆ T" using fim opeTS openin_imp_subset by blast obtain W g where "C ⊆ W" and UW: "openin (top_of_set U) W" and contg: "continuous_on W g" and gim: "g ` W ⊆ T" and geq: "⋀x. x ∈ C ⟹ g x = f x" apply (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf ‹f ` C ⊆ T› cloUC]) using fim by auto show "∃V g. C ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ` V ⊆ S ∧ (∀x∈C. g x = f x)" proof (intro exI conjI) show "C ⊆ W ∩ g -` S" using ‹C ⊆ W› fim geq by blast show "openin (top_of_set U) (W ∩ g -` S)" by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans) show "continuous_on (W ∩ g -` S) g" by (blast intro: continuous_on_subset [OF contg]) show "g ` (W ∩ g -` S) ⊆ S" using gim by blast show "∀x∈C. g x = f x" using geq by blast qed qed lemma ENR_openin: fixes S :: "'a::euclidean_space set" assumes "ENR T" and opeTS: "openin (top_of_set T) S" shows "ENR S" using assms apply (simp add: ENR_ANR) using ANR_openin locally_open_subset by blast lemma ANR_neighborhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR U" "S retract_of T" "openin (top_of_set U) T" shows "ANR S" using ANR_openin ANR_retract_of_ANR assms by blast lemma ENR_neighborhood_retract: fixes S :: "'a::euclidean_space set" assumes "ENR U" "S retract_of T" "openin (top_of_set U) T" shows "ENR S" using ENR_openin ENR_retract_of_ENR assms by blast lemma ANR_rel_interior: fixes S :: "'a::euclidean_space set" shows "ANR S ⟹ ANR(rel_interior S)" by (blast intro: ANR_openin openin_set_rel_interior) lemma ANR_delete: fixes S :: "'a::euclidean_space set" shows "ANR S ⟹ ANR(S - {a})" by (blast intro: ANR_openin openin_delete openin_subtopology_self) lemma ENR_rel_interior: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ENR(rel_interior S)" by (blast intro: ENR_openin openin_set_rel_interior) lemma ENR_delete: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ENR(S - {a})" by (blast intro: ENR_openin openin_delete openin_subtopology_self) lemma open_imp_ENR: "open S ⟹ ENR S" using ENR_def by blast lemma open_imp_ANR: fixes S :: "'a::euclidean_space set" shows "open S ⟹ ANR S" by (simp add: ENR_imp_ANR open_imp_ENR) lemma ANR_ball [iff]: fixes a :: "'a::euclidean_space" shows "ANR(ball a r)" by (simp add: convex_imp_ANR) lemma ENR_ball [iff]: "ENR(ball a r)" by (simp add: open_imp_ENR) lemma AR_ball [simp]: fixes a :: "'a::euclidean_space" shows "AR(ball a r) ⟷ 0 < r" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_cball [iff]: fixes a :: "'a::euclidean_space" shows "ANR(cball a r)" by (simp add: convex_imp_ANR) lemma ENR_cball: fixes a :: "'a::euclidean_space" shows "ENR(cball a r)" using ENR_convex_closed by blast lemma AR_cball [simp]: fixes a :: "'a::euclidean_space" shows "AR(cball a r) ⟷ 0 ≤ r" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_box [iff]: fixes a :: "'a::euclidean_space" shows "ANR(cbox a b)" "ANR(box a b)" by (auto simp: convex_imp_ANR open_imp_ANR) lemma ENR_box [iff]: fixes a :: "'a::euclidean_space" shows "ENR(cbox a b)" "ENR(box a b)" apply (simp add: ENR_convex_closed closed_cbox) by (simp add: open_box open_imp_ENR) lemma AR_box [simp]: "AR(cbox a b) ⟷ cbox a b ≠ {}" "AR(box a b) ⟷ box a b ≠ {}" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_interior: fixes S :: "'a::euclidean_space set" shows "ANR(interior S)" by (simp add: open_imp_ANR) lemma ENR_interior: fixes S :: "'a::euclidean_space set" shows "ENR(interior S)" by (simp add: open_imp_ENR) lemma AR_imp_contractible: fixes S :: "'a::euclidean_space set" shows "AR S ⟹ contractible S" by (simp add: AR_ANR) lemma ENR_imp_locally_compact: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ locally compact S" by (simp add: ENR_ANR) lemma ANR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "ANR S" shows "locally path_connected S" proof - obtain U and T :: "('a × real) set" where "convex U" "U ≠ {}" and UT: "closedin (top_of_set U) T" and "S homeomorphic T" apply (rule homeomorphic_closedin_convex [of S]) using aff_dim_le_DIM [of S] apply auto done then have "locally path_connected T" by (meson ANR_imp_absolute_neighbourhood_retract assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected) then have S: "locally path_connected S" if "openin (top_of_set U) V" "T retract_of V" "U ≠ {}" for V using ‹S homeomorphic T› homeomorphic_locally homeomorphic_path_connectedness by blast show ?thesis using assms apply (clarsimp simp: ANR_def) apply (drule_tac x=U in spec) apply (drule_tac x=T in spec) using ‹S homeomorphic T› ‹U ≠ {}› UT apply (blast intro: S) done qed lemma ANR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "ANR S" shows "locally connected S" using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto lemma AR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "AR S" shows "locally path_connected S" by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms) lemma AR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "AR S" shows "locally connected S" using ANR_imp_locally_connected AR_ANR assms by blast lemma ENR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "ENR S" shows "locally path_connected S" by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms) lemma ENR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "ENR S" shows "locally connected S" using ANR_imp_locally_connected ENR_ANR assms by blast lemma ANR_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ANR S" "ANR T" shows "ANR(S × T)" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: " ('a × 'b) × real ⇒ 'a × 'b" and U C assume "continuous_on C f" and fim: "f ` C ⊆ S × T" and cloUC: "closedin (top_of_set U) C" have contf1: "continuous_on C (fst ∘ f)" by (simp add: ‹continuous_on C f› continuous_on_fst) obtain W1 g where "C ⊆ W1" and UW1: "openin (top_of_set U) W1" and contg: "continuous_on W1 g" and gim: "g ` W1 ⊆ S" and geq: "⋀x. x ∈ C ⟹ g x = (fst ∘ f) x" apply (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› contf1 _ cloUC]) using fim apply auto done have contf2: "continuous_on C (snd ∘ f)" by (simp add: ‹continuous_on C f› continuous_on_snd) obtain W2 h where "C ⊆ W2" and UW2: "openin (top_of_set U) W2" and conth: "continuous_on W2 h" and him: "h ` W2 ⊆ T" and heq: "⋀x. x ∈ C ⟹ h x = (snd ∘ f) x" apply (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf2 _ cloUC]) using fim apply auto done show "∃V g. C ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ` V ⊆ S × T ∧ (∀x∈C. g x = f x)" proof (intro exI conjI) show "C ⊆ W1 ∩ W2" by (simp add: ‹C ⊆ W1› ‹C ⊆ W2›) show "openin (top_of_set U) (W1 ∩ W2)" by (simp add: UW1 UW2 openin_Int) show "continuous_on (W1 ∩ W2) (λx. (g x, h x))" by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1) show "(λx. (g x, h x)) ` (W1 ∩ W2) ⊆ S × T" using gim him by blast show "(∀x∈C. (g x, h x) = f x)" using geq heq by auto qed qed lemma AR_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "AR S" "AR T" shows "AR(S × T)" using assms by (simp add: AR_ANR ANR_Times contractible_Times) subsection ‹Kuhn Simplices› lemma bij_betw_singleton_eq: assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a ∈ A" assumes eq: "(⋀x. x ∈ A ⟹ x ≠ a ⟹ f x = g x)" shows "f a = g a" proof - have "f ` (A - {a}) = g ` (A - {a})" by (intro image_cong) (simp_all add: eq) then have "B - {f a} = B - {g a}" using f g a by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff) moreover have "f a ∈ B" "g a ∈ B" using f g a by (auto simp: bij_betw_def) ultimately show ?thesis by auto qed lemma swap_image: "Fun.swap i j f ` A = (if i ∈ A then (if j ∈ A then f ` A else f ` ((A - {i}) ∪ {j})) else (if j ∈ A then f ` ((A - {j}) ∪ {i}) else f ` A))" by (auto simp: swap_def cong: image_cong_simp) lemmas swap_apply1 = swap_apply(1) lemmas swap_apply2 = swap_apply(2) lemma pointwise_minimal_pointwise_maximal: fixes s :: "(nat ⇒ nat) set" assumes "finite s" and "s ≠ {}" and "∀x∈s. ∀y∈s. x ≤ y ∨ y ≤ x" shows "∃a∈s. ∀x∈s. a ≤ x" and "∃a∈s. ∀x∈s. x ≤ a" using assms proof (induct s rule: finite_ne_induct) case (insert b s) assume *: "∀x∈insert b s. ∀y∈insert b s. x ≤ y ∨ y ≤ x" then obtain u l where "l ∈ s" "∀b∈s. l ≤ b" "u ∈ s" "∀b∈s. b ≤ u" using insert by auto with * show "∃a∈insert b s. ∀x∈insert b s. a ≤ x" "∃a∈insert b s. ∀x∈insert b s. x ≤ a" using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+ qed auto lemma kuhn_labelling_lemma: fixes P Q :: "'a::euclidean_space ⇒ bool" assumes "∀x. P x ⟶ P (f x)" and "∀x. P x ⟶ (∀i∈Basis. Q i ⟶ 0 ≤ x∙i ∧ x∙i ≤ 1)" shows "∃l. (∀x.∀i∈Basis. l x i ≤ (1::nat)) ∧ (∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 0) ⟶ (l x i = 0)) ∧ (∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 1) ⟶ (l x i = 1)) ∧ (∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 0) ⟶ x∙i ≤ f x∙i) ∧ (∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 1) ⟶ f x∙i ≤ x∙i)" proof - { fix x i let ?R = "λy. (P x ∧ Q i ∧ x ∙ i = 0 ⟶ y = (0::nat)) ∧ (P x ∧ Q i ∧ x ∙ i = 1 ⟶ y = 1) ∧ (P x ∧ Q i ∧ y = 0 ⟶ x ∙ i ≤ f x ∙ i) ∧ (P x ∧ Q i ∧ y = 1 ⟶ f x ∙ i ≤ x ∙ i)" { assume "P x" "Q i" "i ∈ Basis" with assms have "0 ≤ f x ∙ i ∧ f x ∙ i ≤ 1" by auto } then have "i ∈ Basis ⟹ ?R 0 ∨ ?R 1" by auto } then show ?thesis unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *) by (subst choice_iff[symmetric])+ blast qed subsubsection ‹The key "counting" observation, somewhat abstracted› lemma kuhn_counting_lemma: fixes bnd compo compo' face S F defines "nF s == card {f∈F. face f s ∧ compo' f}" assumes [simp, intro]: "finite F" ― ‹faces› and [simp, intro]: "finite S" ― ‹simplices› and "⋀f. f ∈ F ⟹ bnd f ⟹ card {s∈S. face f s} = 1" and "⋀f. f ∈ F ⟹ ¬ bnd f ⟹ card {s∈S. face f s} = 2" and "⋀s. s ∈ S ⟹ compo s ⟹ nF s = 1" and "⋀s. s ∈ S ⟹ ¬ compo s ⟹ nF s = 0 ∨ nF s = 2" and "odd (card {f∈F. compo' f ∧ bnd f})" shows "odd (card {s∈S. compo s})" proof - have "(∑s | s ∈ S ∧ ¬ compo s. nF s) + (∑s | s ∈ S ∧ compo s. nF s) = (∑s∈S. nF s)" by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong) also have "… = (∑s∈S. card {f ∈ {f∈F. compo' f ∧ bnd f}. face f s}) + (∑s∈S. card {f ∈ {f∈F. compo' f ∧ ¬ bnd f}. face f s})" unfolding sum.distrib[symmetric] by (subst card_Un_disjoint[symmetric]) (auto simp: nF_def intro!: sum.cong arg_cong[where f=card]) also have "… = 1 * card {f∈F. compo' f ∧ bnd f} + 2 * card {f∈F. compo' f ∧ ¬ bnd f}" using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount) finally have "odd ((∑s | s ∈ S ∧ ¬ compo s. nF s) + card {s∈S. compo s})" using assms(6,8) by simp moreover have "(∑s | s ∈ S ∧ ¬ compo s. nF s) = (∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 0. nF s) + (∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 2. nF s)" using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+ ultimately show ?thesis by auto qed subsubsection ‹The odd/even result for faces of complete vertices, generalized› lemma kuhn_complete_lemma: assumes [simp]: "finite simplices" and face: "⋀f s. face f s ⟷ (∃a∈s. f = s - {a})" and card_s[simp]: "⋀s. s ∈ simplices ⟹ card s = n + 2" and rl_bd: "⋀s. s ∈ simplices ⟹ rl ` s ⊆ {..Suc n}" and bnd: "⋀f s. s ∈ simplices ⟹ face f s ⟹ bnd f ⟹ card {s∈simplices. face f s} = 1" and nbnd: "⋀f s. s ∈ simplices ⟹ face f s ⟹ ¬ bnd f ⟹ card {s∈simplices. face f s} = 2" and odd_card: "odd (card {f. (∃s∈simplices. face f s) ∧ rl ` f = {..n} ∧ bnd f})" shows "odd (card {s∈simplices. (rl ` s = {..Suc n})})" proof (rule kuhn_counting_lemma) have finite_s[simp]: "⋀s. s ∈ simplices ⟹ finite s" by (metis add_is_0 zero_neq_numeral card_infinite assms(3)) let ?F = "{f. ∃s∈simplices. face f s}" have F_eq: "?F = (⋃s∈simplices. ⋃a∈s. {s - {a}})" by (auto simp: face) show "finite ?F" using ‹finite simplices› unfolding F_eq by auto show "card {s ∈ simplices. face f s} = 1" if "f ∈ ?F" "bnd f" for f using bnd that by auto show "card {s ∈ simplices. face f s} = 2" if "f ∈ ?F" "¬ bnd f" for f using nbnd that by auto show "odd (card {f ∈ {f. ∃s∈simplices. face f s}. rl ` f = {..n} ∧ bnd f})" using odd_card by simp fix s assume s[simp]: "s ∈ simplices" let ?S = "{f ∈ {f. ∃s∈simplices. face f s}. face f s ∧ rl ` f = {..n}}" have "?S = (λa. s - {a}) ` {a∈s. rl ` (s - {a}) = {..n}}" using s by (fastforce simp: face) then have card_S: "card ?S = card {a∈s. rl ` (s - {a}) = {..n}}" by (auto intro!: card_image inj_onI) { assume rl: "rl ` s = {..Suc n}" then have inj_rl: "inj_on rl s" by (intro eq_card_imp_inj_on) auto moreover obtain a where "rl a = Suc n" "a ∈ s" by (metis atMost_iff image_iff le_Suc_eq rl) ultimately have n: "{..n} = rl ` (s - {a})" by (auto simp: inj_on_image_set_diff rl) have "{a∈s. rl ` (s - {a}) = {..n}} = {a}" using inj_rl ‹a ∈ s› by (auto simp: n inj_on_image_eq_iff[OF inj_rl]) then show "card ?S = 1" unfolding card_S by simp } { assume rl: "rl ` s ≠ {..Suc n}" show "card ?S = 0 ∨ card ?S = 2" proof cases assume *: "{..n} ⊆ rl ` s" with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}" by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm) then have "¬ inj_on rl s" by (intro pigeonhole) simp then obtain a b where ab: "a ∈ s" "b ∈ s" "rl a = rl b" "a ≠ b" by (auto simp: inj_on_def) then have eq: "rl ` (s - {a}) = rl ` s" by auto with ab have inj: "inj_on rl (s - {a})" by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if) { fix x assume "x ∈ s" "x ∉ {a, b}" then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})" by (auto simp: eq inj_on_image_set_diff[OF inj]) also have "… = rl ` (s - {x})" using ab ‹x ∉ {a, b}› by auto also assume "… = rl ` s" finally have False using ‹x∈s› by auto } moreover { fix x assume "x ∈ {a, b}" with ab have "x ∈ s ∧ rl ` (s - {x}) = rl ` s" by (simp add: set_eq_iff image_iff Bex_def) metis } ultimately have "{a∈s. rl ` (s - {a}) = {..n}} = {a, b}" unfolding rl_s[symmetric] by fastforce with ‹a ≠ b› show "card ?S = 0 ∨ card ?S = 2" unfolding card_S by simp next assume "¬ {..n} ⊆ rl ` s" then have "⋀x. rl ` (s - {x}) ≠ {..n}" by auto then show "card ?S = 0 ∨ card ?S = 2" unfolding card_S by simp qed } qed fact locale kuhn_simplex = fixes p n and base upd and s :: "(nat ⇒ nat) set" assumes base: "base ∈ {..< n} → {..< p}" assumes base_out: "⋀i. n ≤ i ⟹ base i = p" assumes upd: "bij_betw upd {..< n} {..< n}" assumes s_pre: "s = (λi j. if j ∈ upd`{..< i} then Suc (base j) else base j) ` {.. n}" begin definition "enum i j = (if j ∈ upd`{..< i} then Suc (base j) else base j)" lemma s_eq: "s = enum ` {.. n}" unfolding s_pre enum_def[abs_def] .. lemma upd_space: "i < n ⟹ upd i < n" using upd by (auto dest!: bij_betwE) lemma s_space: "s ⊆ {..< n} → {.. p}" proof - { fix i assume "i ≤ n" then have "enum i ∈ {..< n} → {.. p}" proof (induct i) case 0 then show ?case using base by (auto simp: Pi_iff less_imp_le enum_def) next case (Suc i) with base show ?case by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space) qed } then show ?thesis by (auto simp: s_eq) qed lemma inj_upd: "inj_on upd {..< n}" using upd by (simp add: bij_betw_def) lemma inj_enum: "inj_on enum {.. n}" proof - { fix x y :: nat assume "x ≠ y" "x ≤ n" "y ≤ n" with upd have "upd ` {..< x} ≠ upd ` {..< y}" by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def) then have "enum x ≠ enum y" by (auto simp: enum_def fun_eq_iff) } then show ?thesis by (auto simp: inj_on_def) qed lemma enum_0: "enum 0 = base" by (simp add: enum_def[abs_def]) lemma base_in_s: "base ∈ s" unfolding s_eq by (subst enum_0[symmetric]) auto lemma enum_in: "i ≤ n ⟹ enum i ∈ s" unfolding s_eq by auto lemma one_step: assumes a: "a ∈ s" "j < n" assumes *: "⋀a'. a' ∈ s ⟹ a' ≠ a ⟹ a' j = p'" shows "a j ≠ p'" proof assume "a j = p'" with * a have "⋀a'. a' ∈ s ⟹ a' j = p'" by auto then have "⋀i. i ≤ n ⟹ enum i j = p'" unfolding s_eq by auto from this[of 0] this[of n] have "j ∉ upd ` {..< n}" by (auto simp: enum_def fun_eq_iff split: if_split_asm) with upd ‹j < n› show False by (auto simp: bij_betw_def) qed lemma upd_inj: "i < n ⟹ j < n ⟹ upd i = upd j ⟷ i = j" using upd by (auto simp: bij_betw_def inj_on_eq_iff) lemma upd_surj: "upd ` {..< n} = {..< n}" using upd by (auto simp: bij_betw_def) lemma in_upd_image: "A ⊆ {..< n} ⟹ i < n ⟹ upd i ∈ upd ` A ⟷ i ∈ A" using inj_on_image_mem_iff[of upd "{..< n}"] upd by (auto simp: bij_betw_def) lemma enum_inj: "i ≤ n ⟹ j ≤ n ⟹ enum i = enum j ⟷ i = j" using inj_enum by (auto simp: inj_on_eq_iff) lemma in_enum_image: "A ⊆ {.. n} ⟹ i ≤ n ⟹ enum i ∈ enum ` A ⟷ i ∈ A" using inj_on_image_mem_iff[OF inj_enum] by auto lemma enum_mono: "i ≤ n ⟹ j ≤ n ⟹ enum i ≤ enum j ⟷ i ≤ j" by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric]) lemma enum_strict_mono: "i ≤ n ⟹ j ≤ n ⟹ enum i < enum j ⟷ i < j" using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less) lemma chain: "a ∈ s ⟹ b ∈ s ⟹ a ≤ b ∨ b ≤ a" by (auto simp: s_eq enum_mono) lemma less: "a ∈ s ⟹ b ∈ s ⟹ a i < b i ⟹ a < b" using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric]) lemma enum_0_bot: "a ∈ s ⟹ a = enum 0 ⟷ (∀a'∈s. a ≤ a')" unfolding s_eq by (auto simp: enum_mono Ball_def) lemma enum_n_top: "a ∈ s ⟹ a = enum n ⟷ (∀a'∈s. a' ≤ a)" unfolding s_eq by (auto simp: enum_mono Ball_def) lemma enum_Suc: "i < n ⟹ enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))" by (auto simp: fun_eq_iff enum_def upd_inj) lemma enum_eq_p: "i ≤ n ⟹ n ≤ j ⟹ enum i j = p" by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric]) lemma out_eq_p: "a ∈ s ⟹ n ≤ j ⟹ a j = p" unfolding s_eq by (auto simp: enum_eq_p) lemma s_le_p: "a ∈ s ⟹ a j ≤ p" using out_eq_p[of a j] s_space by (cases "j < n") auto lemma le_Suc_base: "a ∈ s ⟹ a j ≤ Suc (base j)" unfolding s_eq by (auto simp: enum_def) lemma base_le: "a ∈ s ⟹ base j ≤ a j" unfolding s_eq by (auto simp: enum_def) lemma enum_le_p: "i ≤ n ⟹ j < n ⟹ enum i j ≤ p" using enum_in[of i] s_space by auto lemma enum_less: "a ∈ s ⟹ i < n ⟹ enum i < a ⟷ enum (Suc i) ≤ a" unfolding s_eq by (auto simp: enum_strict_mono enum_mono) lemma ksimplex_0: "n = 0 ⟹ s = {(λx. p)}" using s_eq enum_def base_out by auto lemma replace_0: assumes "j < n" "a ∈ s" and p: "∀x∈s - {a}. x j = 0" and "x ∈ s" shows "x ≤ a" proof cases assume "x ≠ a" have "a j ≠ 0" using assms by (intro one_step[where a=a]) auto with less[OF ‹x∈s› ‹a∈s›, of j] p[rule_format, of x] ‹x ∈ s› ‹x ≠ a› show ?thesis by auto qed simp lemma replace_1: assumes "j < n" "a ∈ s" and p: "∀x∈s - {a}. x j = p" and "x ∈ s" shows "a ≤ x" proof cases assume "x ≠ a" have "a j ≠ p" using assms by (intro one_step[where a=a]) auto with enum_le_p[of _ j] ‹j < n› ‹a∈s› have "a j < p" by (auto simp: less_le s_eq) with less[OF ‹a∈s› ‹x∈s›, of j] p[rule_format, of x] ‹x ∈ s› ‹x ≠ a› show ?thesis by auto qed simp end locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t for p n b_s u_s s b_t u_t t begin lemma enum_eq: assumes l: "i ≤ l" "l ≤ j" and "j + d ≤ n" assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}" shows "s.enum l = t.enum (l + d)" using l proof (induct l rule: dec_induct) case base then have s: "s.enum i ∈ t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) ∈ s.enum ` {i .. j}" using eq by auto from t ‹i ≤ j› ‹j + d ≤ n› have "s.enum i ≤ t.enum (i + d)" by (auto simp: s.enum_mono) moreover from s ‹i ≤ j› ‹j + d ≤ n› have "t.enum (i + d) ≤ s.enum i" by (auto simp: t.enum_mono) ultimately show ?case by auto next case (step l) moreover from step.prems ‹j + d ≤ n› have "s.enum l < s.enum (Suc l)" "t.enum (l + d) < t.enum (Suc l + d)" by (simp_all add: s.enum_strict_mono t.enum_strict_mono) moreover have "s.enum (Suc l) ∈ t.enum ` {i + d .. j + d}" "t.enum (Suc l + d) ∈ s.enum ` {i .. j}" using step ‹j + d ≤ n› eq by (auto simp: s.enum_inj t.enum_inj) ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))" using ‹j + d ≤ n› by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1]) (auto intro!: s.enum_in t.enum_in) then show ?case by simp qed lemma ksimplex_eq_bot: assumes a: "a ∈ s" "⋀a'. a' ∈ s ⟹ a ≤ a'" assumes b: "b ∈ t" "⋀b'. b' ∈ t ⟹ b ≤ b'" assumes eq: "s - {a} = t - {b}" shows "s = t" proof cases assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp next assume "n ≠ 0" have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)" "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)" using ‹n ≠ 0› by (simp_all add: s.enum_Suc t.enum_Suc) moreover have e0: "a = s.enum 0" "b = t.enum 0" using a b by (simp_all add: s.enum_0_bot t.enum_0_bot) moreover { fix j assume "0 < j" "j ≤ n" moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}" unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj) ultimately have "s.enum j = t.enum j" using enum_eq[of "1" j n 0] eq by auto } note enum_eq = this then have "s.enum (Suc 0) = t.enum (Suc 0)" using ‹n ≠ 0› by auto moreover { fix j assume "Suc j < n" with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"] have "u_s (Suc j) = u_t (Suc j)" using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"] by (auto simp: fun_eq_iff split: if_split_asm) } then have "⋀j. 0 < j ⟹ j < n ⟹ u_s j = u_t j" by (auto simp: gr0_conv_Suc) with ‹n ≠ 0› have "u_t 0 = u_s 0" by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto ultimately have "a = b" by simp with assms show "s = t" by auto qed lemma ksimplex_eq_top: assumes a: "a ∈ s" "⋀a'. a' ∈ s ⟹ a' ≤ a" assumes b: "b ∈ t" "⋀b'. b' ∈ t ⟹ b' ≤ b" assumes eq: "s - {a} = t - {b}" shows "s = t" proof (cases n) assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp next case (Suc n') have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))" "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))" using Suc by (simp_all add: s.enum_Suc t.enum_Suc) moreover have en: "a = s.enum n" "b = t.enum n" using a b by (simp_all add: s.enum_n_top t.enum_n_top) moreover { fix j assume "j < n" moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}" unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc) ultimately have "s.enum j = t.enum j" using enum_eq[of "0" j n' 0] eq Suc by auto } note enum_eq = this then have "s.enum n' = t.enum n'" using Suc by auto moreover { fix j assume "j < n'" with enum_eq[of j] enum_eq[of "Suc j"] have "u_s j = u_t j" using s.enum_Suc[of j] t.enum_Suc[of j] by (auto simp: Suc fun_eq_iff split: if_split_asm) } then have "⋀j. j < n' ⟹ u_s j = u_t j" by (auto simp: gr0_conv_Suc) then have "u_t n' = u_s n'" by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc) ultimately have "a = b" by simp with assms show "s = t" by auto qed end inductive ksimplex for p n :: nat where ksimplex: "kuhn_simplex p n base upd s ⟹ ksimplex p n s" lemma finite_ksimplexes: "finite {s. ksimplex p n s}" proof (rule finite_subset) { fix a s assume "ksimplex p n s" "a ∈ s" then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p n b u s . from s_space ‹a ∈ s› out_eq_p[OF ‹a ∈ s›] have "a ∈ (λf x. if n ≤ x then p else f x) ` ({..< n} →⇩_{E}{.. p})" by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm intro!: bexI[of _ "restrict a {..< n}"]) } then show "{s. ksimplex p n s} ⊆ Pow ((λf x. if n ≤ x then p else f x) ` ({..< n} →⇩_{E}{.. p}))" by auto qed (simp add: finite_PiE) lemma ksimplex_card: assumes "ksimplex p n s" shows "card s = Suc n" using assms proof cases case (ksimplex u b) then interpret kuhn_simplex p n u b s . show ?thesis by (simp add: card_image s_eq inj_enum) qed lemma simplex_top_face: assumes "0 < p" "∀x∈s'. x n = p" shows "ksimplex p n s' ⟷ (∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a})" using assms proof safe fix s a assume "ksimplex p (Suc n) s" and a: "a ∈ s" and na: "∀x∈s - {a}. x n = p" then show "ksimplex p n (s - {a})" proof cases case (ksimplex base upd) then interpret kuhn_simplex p "Suc n" base upd "s" . have "a n < p" using one_step[of a n p] na ‹a∈s› s_space by (auto simp: less_le) then have "a = enum 0" using ‹a ∈ s› na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n]) then have s_eq: "s - {a} = enum ` Suc ` {.. n}" using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq) then have "enum 1 ∈ s - {a}" by auto then have "upd 0 = n" using ‹a n < p› ‹a = enum 0› na[rule_format, of "enum 1"] by (auto simp: fun_eq_iff enum_Suc split: if_split_asm) then have "bij_betw upd (Suc ` {..< n}) {..< n}" using upd by (subst notIn_Un_bij_betw3[where b=0]) (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0) then have "bij_betw (upd∘Suc) {..<n} {..<n}" by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def) have "a n = p - 1" using enum_Suc[of 0] na[rule_format, OF ‹enum 1 ∈ s - {a}›] ‹a = enum 0› by (auto simp: ‹upd 0 = n›) show ?thesis proof (rule ksimplex.intros, standard) show "bij_betw (upd∘Suc) {..< n} {..< n}" by fact show "base(n := p) ∈ {..<n} → {..<p}" "⋀i. n≤i ⟹ (base(n := p)) i = p" using base base_out by (auto simp: Pi_iff) have "⋀i. Suc ` {..< i} = {..< Suc i} - {0}" by (auto simp: image_iff Ball_def) arith then have upd_Suc: "⋀i. i ≤ n ⟹ (upd∘Suc) ` {..< i} = upd ` {..< Suc i} - {n}" using ‹upd 0 = n› upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj) have n_in_upd: "⋀i. n ∈ upd ` {..< Suc i}" using ‹upd 0 = n› by auto define f' where "f' i j = (if j ∈ (upd∘Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j { fix x i assume i [arith]: "i ≤ n" with upd_Suc have "(upd ∘ Suc) ` {..<i} = upd ` {..<Suc i} - {n}" . with ‹a n < p› ‹a = enum 0› ‹upd 0 = n› ‹a n = p - 1› have "enum (Suc i) x = f' i x" by (auto simp add: f'_def enum_def) } then show "s - {a} = f' ` {.. n}" unfolding s_eq image_comp by (intro image_cong) auto qed qed next assume "ksimplex p n s'" and *: "∀x∈s'. x n = p" then show "∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a}" proof cases case (ksimplex base upd) then interpret kuhn_simplex p n base upd s' . define b where "b = base (n := p - 1)" define u where "u i = (case i of 0 ⇒ n | Suc i ⇒ upd i)" for i have "ksimplex p (Suc n) (s' ∪ {b})" proof (rule ksimplex.intros, standard) show "b ∈ {..<Suc n} → {..<p}" using base ‹0 < p› unfolding lessThan_Suc b_def by (auto simp: PiE_iff) show "⋀i. Suc n ≤ i ⟹ b i = p" using base_out by (auto simp: b_def) have "bij_betw u (Suc ` {..< n} ∪ {0}) ({..<n} ∪ {u 0})" using upd by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def) then show "bij_betw u {..<Suc n} {..<Suc n}" by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0) define f' where "f' i j = (if j ∈ u`{..< i} then Suc (b j) else b j)" for i j have u_eq: "⋀i. i ≤ n ⟹ u ` {..< Suc i} = upd ` {..< i} ∪ { n }" by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith { fix x have "x ≤ n ⟹ n ∉ upd ` {..<x}" using upd_space by (simp add: image_iff neq_iff) } note n_not_upd = this have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} ∪ {0})" unfolding atMost_Suc_eq_insert_0 by simp also have "… = (f' ∘ Suc) ` {.. n} ∪ {b}" by (auto simp: f'_def) also have "(f' ∘ Suc) ` {.. n} = s'" using ‹0 < p› base_out[of n] unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd) finally show "s' ∪ {b} = f' ` {.. Suc n}" .. qed moreover have "b ∉ s'" using * ‹0 < p› by (auto simp: b_def) ultimately show ?thesis by auto qed qed lemma ksimplex_replace_0: assumes s: "ksimplex p n s" and a: "a ∈ s" assumes j: "j < n" and p: "∀x∈s - {a}. x j = 0" shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1" using s proof cases case (ksimplex b_s u_s) { fix t b assume "ksimplex p n t" then obtain b_t u_t where "kuhn_simplex p n b_t u_t t" by (auto elim: ksimplex.cases) interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t by intro_locales fact+ assume b: "b ∈ t" "t - {b} = s - {a}" with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t" by (intro ksimplex_eq_top[of a b]) auto } then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}" using s ‹a ∈ s› by auto then show ?thesis by simp qed lemma ksimplex_replace_1: assumes s: "ksimplex p n s" and a: "a ∈ s" assumes j: "j < n" and p: "∀x∈s - {a}. x j = p" shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1" using s proof cases case (ksimplex b_s u_s) { fix t b assume "ksimplex p n t" then obtain b_t u_t where "kuhn_simplex p n b_t u_t t" by (auto elim: ksimplex.cases) interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t by intro_locales fact+ assume b: "b ∈ t" "t - {b} = s - {a}" with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t" by (intro ksimplex_eq_bot[of a b]) auto } then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}" using s ‹a ∈ s› by auto then show ?thesis by simp qed lemma card_2_exists: "card s = 2 ⟷ (∃x∈s. ∃y∈s. x ≠ y ∧ (∀z∈s. z = x ∨ z = y))" by (auto simp: card_Suc_eq eval_nat_numeral) lemma ksimplex_replace_2: assumes s: "ksimplex p n s" and "a ∈ s" and "n ≠ 0" and lb: "∀j<n. ∃x∈s - {a}. x j ≠ 0" and ub: "∀j<n. ∃x∈s - {a}. x j ≠ p" shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 2" using s proof cases case (ksimplex base upd) then interpret kuhn_simplex p n base upd s . from ‹a ∈ s› obtain i where "i ≤ n" "a = enum i" unfolding s_eq by auto from ‹i ≤ n› have "i = 0 ∨ i = n ∨ (0 < i ∧ i < n)" by linarith then have "∃!s'. s' ≠ s ∧ ksimplex p n s' ∧ (∃b∈s'. s - {a} = s'- {b})" proof (elim disjE conjE) assume "i = 0" define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i let ?upd = "upd ∘ rot" have rot: "bij_betw rot {..< n} {..< n}" by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def) arith+ from rot upd have "bij_betw ?upd {..<n} {..<n}" by (rule bij_betw_trans) define f' where [abs_def]: "f' i j = (if j ∈ ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j interpret b: kuhn_simplex p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}" proof from ‹a = enum i› ub ‹n ≠ 0› ‹i = 0› obtain i' where "i' ≤ n" "enum i' ≠ enum 0" "enum i' (upd 0) ≠ p" unfolding s_eq by (auto intro: upd_space simp: enum_inj) then have "enum 1 ≤ enum i'" "enum i' (upd 0) < p" using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space) then have "enum 1 (upd 0) < p" by (auto simp: le_fun_def intro: le_less_trans) then show "enum (Suc 0) ∈ {..<n} → {..<p}" using base ‹n ≠ 0› by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space) { fix i assume "n ≤ i" then show "enum (Suc 0) i = p" using ‹n ≠ 0› by (auto simp: enum_eq_p) } show "bij_betw ?upd {..<n} {..<n}" by fact qed (simp add: f'_def) have ks_f': "ksimplex p n (f' ` {.. n})" by rule unfold_locales have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] .. with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp have f'_eq_enum: "f' j = enum (Suc j)" if "j < n" for j proof - from that have "rot ` {..< j} = {0 <..< Suc j}" by (auto simp: rot_def image_Suc_lessThan cong: image_cong_simp) with that ‹n ≠ 0› show ?thesis by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric]) (auto simp add: upd_inj) qed then have "enum ` Suc ` {..< n} = f' ` {..< n}" by (force simp: enum_inj) also have "Suc ` {..< n} = {.. n} - {0}" by (auto simp: image_iff Ball_def) arith also have "{..< n} = {.. n} - {n}" by auto finally have eq: "s - {a} = f' ` {.. n} - {f' n}" unfolding s_eq ‹a = enum i› ‹i = 0› by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f']) have "enum 0 < f' 0" using ‹n ≠ 0› by (simp add: enum_strict_mono f'_eq_enum) also have "… < f' n" using ‹n ≠ 0› b.enum_strict_mono[of 0 n] unfolding b_enum by simp finally have "a ≠ f' n" using ‹a = enum i› ‹i = 0› by auto { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}" obtain b u where "kuhn_simplex p n b u t" using ‹ksimplex p n t› by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b u t . { fix x assume "x ∈ s" "x ≠ a" then have "x (upd 0) = enum (Suc 0) (upd 0)" by (auto simp: ‹a = enum i› ‹i = 0› s_eq enum_def enum_inj) } then have eq_upd0: "∀x∈t-{c}. x (upd 0) = enum (Suc 0) (upd 0)" unfolding eq_sma[symmetric] by auto then have "c (upd 0) ≠ enum (Suc 0) (upd 0)" using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: upd_space) then have "c (upd 0) < enum (Suc 0) (upd 0) ∨ c (upd 0) > enum (Suc 0) (upd 0)" by auto then have "t = s ∨ t = f' ` {..n}" proof (elim disjE conjE) assume *: "c (upd 0) < enum (Suc 0) (upd 0)" interpret st: kuhn_simplex_pair p n base upd s b u t .. { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x" by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) } note top = this have "s = t" using ‹a = enum i› ‹i = 0› ‹c ∈ t› by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma]) (auto simp: s_eq enum_mono t.s_eq t.enum_mono top) then show ?thesis by simp next assume *: "c (upd 0) > enum (Suc 0) (upd 0)" interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}" b u t .. have eq: "f' ` {..n} - {f' n} = t - {c}" using eq_sma eq by simp { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c" by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) } note top = this have "f' ` {..n} = t" using ‹a = enum i› ‹i = 0› ‹c ∈ t› by (intro st.ksimplex_eq_top[OF _ _ _ _ eq]) (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top) then show ?thesis by simp qed } with ks_f' eq ‹a ≠ f' n› ‹n ≠ 0› show ?thesis apply (intro ex1I[of _ "f' ` {.. n}"]) apply auto [] apply metis done next assume "i = n" from ‹n ≠ 0› obtain n' where n': "n = Suc n'" by (cases n) auto define rot where "rot i = (case i of 0 ⇒ n' | Suc i ⇒ i)" for i let ?upd = "upd ∘ rot" have rot: "bij_betw rot {..< n} {..< n}" by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits) arith from rot upd have "bij_betw ?upd {..<n} {..<n}" by (rule bij_betw_trans) define b where "b = base (upd n' := base (upd n') - 1)" define f' where [abs_def]: "f' i j = (if j ∈ ?upd`{..< i} then Suc (b j) else b j)" for i j interpret b: kuhn_simplex p n b "upd ∘ rot" "f' ` {.. n}" proof { fix i assume "n ≤ i" then show "b i = p" using base_out[of i] upd_space[of n'] by (auto simp: b_def n') } show "b ∈ {..<n} → {..<p}" using base ‹n ≠ 0› upd_space[of n'] by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n') show "bij_betw ?upd {..<n} {..<n}" by fact qed (simp add: f'_def) have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] .. have ks_f': "ksimplex p n (b.enum ` {.. n})" unfolding f' by rule unfold_locales have "0 < n" using ‹n ≠ 0› by auto { from ‹a = enum i› ‹n ≠ 0› ‹i = n› lb upd_space[of n'] obtain i' where "i' ≤ n" "enum i' ≠ enum n" "0 < enum i' (upd n')" unfolding s_eq by (auto simp: enum_inj n') moreover have "enum i' (upd n') = base (upd n')" unfolding enum_def using ‹i' ≤ n› ‹enum i' ≠ enum n› by (auto simp: n' upd_inj enum_inj) ultimately have "0 < base (upd n')" by auto } then have benum1: "b.enum (Suc 0) = base" unfolding b.enum_Suc[OF ‹0<n›] b.enum_0 by (auto simp: b_def rot_def) have [simp]: "⋀j. Suc j < n ⟹ rot ` {..< Suc j} = {n'} ∪ {..< j}" by (auto simp: rot_def image_iff Ball_def split: nat.splits) have rot_simps: "⋀j. rot (Suc j) = j" "rot 0 = n'" by (simp_all add: rot_def) { fix j assume j: "Suc j ≤ n" then have "b.enum (Suc j) = enum j" by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) } note b_enum_eq_enum = this then have "enum ` {..< n} = b.enum ` Suc ` {..< n}" by (auto simp: image_comp intro!: image_cong) also have "Suc ` {..< n} = {.. n} - {0}" by (auto simp: image_iff Ball_def) arith also have "{..< n} = {.. n} - {n}" by auto finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}" unfolding s_eq ‹a = enum i› ‹i = n› using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"] inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"] by (simp add: comp_def) have "b.enum 0 ≤ b.enum n" by (simp add: b.enum_mono) also have "b.enum n < enum n" using ‹n ≠ 0› by (simp add: enum_strict_mono b_enum_eq_enum n') finally have "a ≠ b.enum 0" using ‹a = enum i› ‹i = n› by auto { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}" obtain b' u where "kuhn_simplex p n b' u t" using ‹ksimplex p n t› by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b' u t . { fix x assume "x ∈ s" "x ≠ a" then have "x (upd n') = enum n' (upd n')" by (auto simp: ‹a = enum i› n' ‹i = n› s_eq enum_def enum_inj in_upd_image) } then have eq_upd0: "∀x∈t-{c}. x (upd n') = enum n' (upd n')" unfolding eq_sma[symmetric] by auto then have "c (upd n') ≠ enum n' (upd n')" using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: n' upd_space[unfolded n']) then have "c (upd n') < enum n' (upd n') ∨ c (upd n') > enum n' (upd n')" by auto then have "t = s ∨ t = b.enum ` {..n}" proof (elim disjE conjE) assume *: "c (upd n') > enum n' (upd n')" interpret st: kuhn_simplex_pair p n base upd s b' u t .. { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c" by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) } note top = this have "s = t" using ‹a = enum i› ‹i = n› ‹c ∈ t› by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma]) (auto simp: s_eq enum_mono t.s_eq t.enum_mono top) then show ?thesis by simp next assume *: "c (upd n') < enum n' (upd n')" interpret st: kuhn_simplex_pair p n b "upd ∘ rot" "f' ` {.. n}" b' u t .. have eq: "f' ` {..n} - {b.enum 0} = t - {c}" using eq_sma eq f' by simp { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x" by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) } note bot = this have "f' ` {..n} = t" using ‹a = enum i› ‹i = n› ‹c ∈ t› by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq]) (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot) with f' show ?thesis by simp qed } with ks_f' eq ‹a ≠ b.enum 0› ‹n ≠ 0› show ?thesis apply (intro ex1I[of _ "b.enum ` {.. n}"]) apply auto [] apply metis done next assume i: "0 < i" "i < n" define i' where "i' = i - 1" with i have "Suc i' < n" by simp with i have Suc_i': "Suc i' = i" by (simp add: i'_def) let ?upd = "Fun.swap i' i upd" from i upd have "bij_betw ?upd {..< n} {..< n}" by (subst bij_betw_swap_iff) (auto simp: i'_def) define f' where [abs_def]: "f' i j = (if j ∈ ?upd`{..< i} then Suc (base j) else base j)" for i j interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}" proof show "base ∈ {..<n} → {..<p}" by (rule base) { fix i assume "n ≤ i" then show "base i = p" by (rule base_out) } show "bij_betw ?upd {..<n} {..<n}" by fact qed (simp add: f'_def) have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] .. have ks_f': "ksimplex p n (b.enum ` {.. n})" unfolding f' by rule unfold_locales have "{i} ⊆ {..n}" using i by auto { fix j assume "j ≤ n" moreover have "j < i ∨ i = j ∨ i < j" by arith moreover note i ultimately have "enum j = b.enum j ⟷ j ≠ i" unfolding enum_def[abs_def] b.enum_def[abs_def] by (auto simp: fun_eq_iff swap_image i'_def in_upd_image inj_on_image_set_diff[OF inj_upd]) } note enum_eq_benum = this then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})" by (intro image_cong) auto then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}" unfolding s_eq ‹a = enum i› using inj_on_image_set_diff[OF inj_enum Diff_subset ‹{i} ⊆ {..n}›] inj_on_image_set_diff[OF b.inj_enum Diff_subset ‹{i} ⊆ {..n}›] by (simp add: comp_def) have "a ≠ b.enum i" using ‹a = enum i› enum_eq_benum i by auto { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}" obtain b' u where "kuhn_simplex p n b' u t" using ‹ksimplex p n t› by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b' u t . have "enum i' ∈ s - {a}" "enum (i + 1) ∈ s - {a}" using ‹a = enum i› i enum_in by (auto simp: enum_inj i'_def) then obtain l k where l: "t.enum l = enum i'" "l ≤ n" "t.enum l ≠ c" and k: "t.enum k = enum (i + 1)" "k ≤ n" "t.enum k ≠ c" unfolding eq_sma by (auto simp: t.s_eq) with i have "t.enum l < t.enum k" by (simp add: enum_strict_mono i'_def) with ‹l ≤ n› ‹k ≤ n› have "l < k" by (simp add: t.enum_strict_mono) { assume "Suc l = k" have "enum (Suc (Suc i')) = t.enum (Suc l)" using i by (simp add: k ‹Suc l = k› i'_def) then have False using ‹l < k› ‹k ≤ n› ‹Suc i' < n› by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm) (metis Suc_lessD n_not_Suc_n upd_inj) } with ‹l < k› have "Suc l < k" by arith have c_eq: "c = t.enum (Suc l)" proof (rule ccontr) assume "c ≠ t.enum (Suc l)" then have "t.enum (Suc l) ∈ s - {a}" using ‹l < k› ‹k ≤ n› by (simp add: t.s_eq eq_sma) then obtain j where "t.enum (Suc l) = enum j" "j ≤ n" "enum j ≠ enum i" unfolding s_eq ‹a = enum i› by auto with i have "t.enum (Suc l) ≤ t.enum l ∨ t.enum k ≤ t.enum (Suc l)" by (auto simp: i'_def enum_mono enum_inj l k) with ‹Suc l < k› ‹k ≤ n› show False by (simp add: t.enum_mono) qed { have "t.enum (Suc (Suc l)) ∈ s - {a}" unfolding eq_sma c_eq t.s_eq using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_inj) then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j ≤ n" "j ≠ i" by (auto simp: s_eq ‹a = enum i›) moreover have "enum i' < t.enum (Suc (Suc l))" unfolding l(1)[symmetric] using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_strict_mono) ultimately have "i' < j" using i by (simp add: enum_strict_mono i'_def) with ‹j ≠ i› ‹j ≤ n› have "t.enum k ≤ t.enum (Suc (Suc l))" unfolding i'_def by (simp add: enum_mono k eq) then have "k ≤ Suc (Suc l)" using ‹k ≤ n› ‹Suc l < k› by (simp add: t.enum_mono) } with ‹Suc l < k› have "Suc (Suc l) = k" by simp then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))" using i by (simp add: k i'_def) also have "… = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))" using ‹Suc l < k› ‹k ≤ n› by (simp add: t.enum_Suc l t.upd_inj) finally have "(u l = upd i' ∧ u (Suc l) = upd (Suc i')) ∨ (u l = upd (Suc i') ∧ u (Suc l) = upd i')" using ‹Suc i' < n› by (auto simp: enum_Suc fun_eq_iff split: if_split_asm) then have "t = s ∨ t = b.enum ` {..n}" proof (elim disjE conjE) assume u: "u l = upd i'" have "c = t.enum (Suc l)" unfolding c_eq .. also have "t.enum (Suc l) = enum (Suc i')" using u ‹l < k› ‹k ≤ n› ‹Suc i' < n› by (simp add: enum_Suc t.enum_Suc l) also have "… = a" using ‹a = enum i› i by (simp add: i'_def) finally show ?thesis using eq_sma ‹a ∈ s› ‹c ∈ t› by auto next assume u: "u l = upd (Suc i')" define B where "B = b.enum ` {..n}" have "b.enum i' = enum i'" using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc) have "c = t.enum (Suc l)" unfolding c_eq .. also have "t.enum (Suc l) = b.enum (Suc i')" using u ‹l < k› ‹k ≤ n› ‹Suc i' < n› by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc ‹b.enum i' = enum i'› swap_apply1) (simp add: Suc_i') also have "… = b.enum i" using i by (simp add: i'_def) finally have "c = b.enum i" . then have "t - {c} = B - {c}" "c ∈ B" unfolding eq_sma[symmetric] eq B_def using i by auto with ‹c ∈ t› have "t = B" by auto then show ?thesis by (simp add: B_def) qed } with ks_f' eq ‹a ≠ b.enum i› ‹n ≠ 0› ‹i ≤ n› show ?thesis apply (intro ex1I[of _ "b.enum ` {.. n}"]) apply auto [] apply metis done qed then show ?thesis using s ‹a ∈ s› by (simp add: card_2_exists Ex1_def) metis qed text ‹Hence another step towards concreteness.› lemma kuhn_simplex_lemma: assumes "∀s. ksimplex p (Suc n) s ⟶ rl ` s ⊆ {.. Suc n}" and "odd (card {f. ∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ (f = s - {a}) ∧ rl ` f = {..n} ∧ ((∃j≤n. ∀x∈f. x j = 0) ∨ (∃j≤n. ∀x∈f. x j = p))})" shows "odd (card {s. ksimplex p (Suc n) s ∧ rl ` s = {..Suc n}})" proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq, where bnd="λf. (∃j∈{..n}. ∀x∈f. x j = 0) ∨ (∃j∈{..n}. ∀x∈f. x j = p)"], safe del: notI) have *: "⋀x y. x = y ⟹ odd (card x) ⟹ odd (card y)" by auto show "odd (card {f. (∃s∈{s. ksimplex p (Suc n) s}. ∃a∈s. f = s - {a}) ∧ rl ` f = {..n} ∧ ((∃j∈{..n}. ∀x∈f. x j = 0) ∨ (∃j∈{..n}. ∀x∈f. x j = p))})" apply (rule *[OF _ assms(2)]) apply (auto simp: atLeast0AtMost) done next fix s assume s: "ksimplex p (Suc n) s" then show "card s = n + 2" by (simp add: ksimplex_card) fix a assume a: "a ∈ s" then show "rl a ≤ Suc n" using assms(1) s by (auto simp: subset_eq) let ?S = "{t. ksimplex p (Suc n) t ∧ (∃b∈t. s - {a} = t - {b})}" { fix j assume j: "j ≤ n" "∀x∈s - {a}. x j = 0" with s a show "card ?S = 1" using ksimplex_replace_0[of p "n + 1" s a j] by (subst eq_commute) simp } { fix j assume j: "j ≤ n" "∀x∈s - {a}. x j = p" with s a show "card ?S = 1" using ksimplex_replace_1[of p "n + 1" s a j] by (subst eq_commute) simp } { assume "card ?S ≠ 2" "¬ (∃j∈{..n}. ∀x∈s - {a}. x j = p)" with s a show "∃j∈{..n}. ∀x∈s - {a}. x j = 0" using ksimplex_replace_2[of p "n + 1" s a] by (subst (asm) eq_commute) auto } qed subsubsection ‹Reduced labelling› definition reduced :: "nat ⇒ (nat ⇒ nat) ⇒ nat" where "reduced n x = (LEAST k. k = n ∨ x k ≠ 0)" lemma reduced_labelling: shows "reduced n x ≤ n" and "∀i<reduced n x. x i = 0" and "reduced n x = n ∨ x (reduced n x) ≠ 0" proof - show "reduced n x ≤ n" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto show "∀i<reduced n x. x i = 0" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+ show "reduced n x = n ∨ x (reduced n x) ≠ 0" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+ qed lemma reduced_labelling_unique: "r ≤ n ⟹ ∀i<r. x i = 0 ⟹ r = n ∨ x r ≠ 0 ⟹ reduced n x = r" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+ lemma reduced_labelling_zero: "j < n ⟹ x j = 0 ⟹ reduced n x ≠ j" using reduced_labelling[of n x] by auto lemma reduce_labelling_zero[simp]: "reduced 0 x = 0" by (rule reduced_labelling_unique) auto lemma reduced_labelling_nonzero: "j < n ⟹ x j ≠ 0 ⟹ reduced n x ≤ j" using reduced_labelling[of n x] by (elim allE[where x=j]) auto lemma reduced_labelling_Suc: "reduced (Suc n) x ≠ Suc n ⟹ reduced (Suc n) x = reduced n x" using reduced_labelling[of "Suc n" x] by (intro reduced_labelling_unique[symmetric]) auto lemma complete_face_top: assumes "∀x∈f. ∀j≤n. x j = 0 ⟶ lab x j = 0" and "∀x∈f. ∀j≤n. x j = p ⟶ lab x j = 1" and eq: "(reduced (Suc n) ∘ lab) ` f = {..n}" shows "((∃j≤n. ∀x∈f. x j = 0) ∨ (∃j≤n. ∀x∈f. x j = p)) ⟷ (∀x∈f. x n = p)" proof (safe del: disjCI) fix x j assume j: "j ≤ n" "∀x∈f. x j = 0" { fix x assume "x ∈ f" with assms j have "reduced (Suc n) (lab x) ≠ j" by (intro reduced_labelling_zero) auto } moreover have "j ∈ (reduced (Suc n) ∘ lab) ` f" using j eq by auto ultimately show "x n = p" by force next fix x j assume j: "j ≤ n" "∀x∈f. x j = p" and x: "x ∈ f" have "j = n" proof (rule ccontr) assume "¬ ?thesis" { fix x assume "x ∈ f" with assms j have "reduced (Suc n) (lab x) ≤ j" by (intro reduced_labelling_nonzero) auto then have "reduced (Suc n) (lab x) ≠ n" using ‹j ≠ n› ‹j ≤ n› by simp } moreover have "n ∈ (reduced (Suc n) ∘ lab) ` f" using eq by auto ultimately show False by force qed moreover have "j ∈ (reduced (Suc n) ∘ lab) ` f" using j eq by auto ultimately show "x n = p" using j x by auto qed auto text ‹Hence we get just about the nice induction.› lemma kuhn_induction: assumes "0 < p" and lab_0: "∀x. ∀j≤n. (∀j. x j ≤ p) ∧ x j = 0 ⟶ lab x j = 0" and lab_1: "∀x. ∀j≤n. (∀j. x j ≤ p) ∧ x j = p ⟶ lab x j = 1" and odd: "odd (card {s. ksimplex p n s ∧ (reduced n∘lab) ` s = {..n}})" shows "odd (card {s. ksimplex p (Suc n) s ∧ (reduced (Suc n)∘lab) ` s = {..Suc n}})" proof - let ?rl = "reduced (Suc n) ∘ lab" and ?ext = "λf v. ∃j≤n. ∀x∈f. x j = v" let ?ext = "λs. (∃j≤n. ∀x∈s. x j = 0) ∨ (∃j≤n. ∀x∈s. x j = p)" have "∀s. ksimplex p (Suc n) s ⟶ ?rl ` s ⊆ {..Suc n}" by (simp add: reduced_labelling subset_eq) moreover have "{s. ksimplex p n s ∧ (reduced n ∘ lab) ` s = {..n}} = {f. ∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ f = s - {a} ∧ ?rl ` f = {..n} ∧ ?ext f}" proof (intro set_eqI, safe del: disjCI equalityI disjE) fix s assume s: "ksimplex p n s" and rl: "(reduced n ∘ lab) ` s = {..n}" from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p n u b s . have all_eq_p: "∀x∈s. x n = p" by (auto simp: out_eq_p) moreover { fix x assume "x ∈ s" with lab_1[rule_format, of n x] all_eq_p s_le_p[of x] have "?rl x ≤ n" by (auto intro!: reduced_labelling_nonzero) then have "?rl x = reduced n (lab x)" by (auto intro!: reduced_labelling_Suc) } then have "?rl ` s = {..n}" using rl by (simp cong: image_cong) moreover obtain t a where "ksimplex p (Suc n) t" "a ∈ t" "s = t - {a}" using s unfolding simplex_top_face[OF ‹0 < p› all_eq_p] by auto ultimately show "∃t a. ksimplex p (Suc n) t ∧ a ∈ t ∧ s = t - {a} ∧ ?rl ` s = {..n} ∧ ?ext s" by auto next fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}" and a: "a ∈ s" and "?ext (s - {a})" from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p "Suc n" u b s . have all_eq_p: "∀x∈s. x (Suc n) = p" by (auto simp: out_eq_p) { fix x assume "x ∈ s - {a}" then have "?rl x ∈ ?rl ` (s - {a})" by auto then have "?rl x ≤ n" unfolding rl by auto then have "?rl x = reduced n (lab x)" by (auto intro!: reduced_labelling_Suc) } then show rl': "(reduced n∘lab) ` (s - {a}) = {..n}" unfolding rl[symmetric] by (intro image_cong) auto from ‹?ext (s - {a})› have all_eq_p: "∀x∈s - {a}. x n = p" proof (elim disjE exE conjE) fix j assume "j ≤ n" "∀x∈s - {a}. x j = 0" with lab_0[rule_format, of j] all_eq_p s_le_p have "⋀x. x ∈ s - {a} ⟹ reduced (Suc n) (lab x) ≠ j" by (intro reduced_labelling_zero) auto moreover have "j ∈ ?rl ` (s - {a})" using ‹j ≤ n› unfolding rl by auto ultimately show ?thesis by force next fix j assume "j ≤ n" and eq_p: "∀x∈s - {a}. x j = p" show ?thesis proof cases assume "j = n" with eq_p show ?thesis by simp next assume "j ≠ n" { fix x assume x: "x ∈ s - {a}" have "reduced n (lab x) ≤ j" proof (rule reduced_labelling_nonzero) show "lab x j ≠ 0" using lab_1[rule_format, of j x] x s_le_p[of x] eq_p ‹j ≤ n› by auto show "j < n" using ‹j ≤ n› ‹j ≠ n› by simp qed then have "reduced n (lab x) ≠ n" using ‹j ≤ n› ‹j ≠ n› by simp } moreover have "n ∈ (reduced n∘lab) ` (s - {a})" unfolding rl' by auto ultimately show ?thesis by force qed qed show "ksimplex p n (s - {a})" unfolding simplex_top_face[OF ‹0 < p› all_eq_p] using s a by auto qed ultimately show ?thesis using assms by (intro kuhn_simplex_lemma) auto qed text ‹And so we get the final combinatorial result.› lemma ksimplex_0: "ksimplex p 0 s ⟷ s = {(λx. p)}" proof assume "ksimplex p 0 s" then show "s = {(λx. p)}" by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases) next assume s: "s = {(λx. p)}" show "ksimplex p 0 s" proof (intro ksimplex, unfold_locales) show "(λ_. p) ∈ {..<0::nat} → {..<p}" by auto show "bij_betw id {..<0} {..<0}" by simp qed (auto simp: s) qed lemma kuhn_combinatorial: assumes "0 < p" and "∀x j. (∀j. x j ≤ p) ∧ j < n ∧ x j = 0 ⟶ lab x j = 0" and "∀x j. (∀j. x j ≤ p) ∧ j < n ∧ x j = p ⟶ lab x j = 1" shows "odd (card {s. ksimplex p n s ∧ (reduced n∘lab) ` s = {..n}})" (is "odd (card (?M n))") using assms proof (induct n) case 0 then show ?case by (simp add: ksimplex_0 cong: conj_cong) next case (Suc n) then have "odd (card (?M n))" by force with Suc show ?case using kuhn_induction[of p n] by (auto simp: comp_def) qed lemma kuhn_lemma: fixes n p :: nat assumes "0 < p" and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. label x i = (0::nat) ∨ label x i = 1)" and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = 0 ⟶ label x i = 0)" and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = p ⟶ label x i = 1)" obtains q where "∀i<n. q i < p" and "∀i<n. ∃r s. (∀j<n. q j ≤ r j ∧ r j ≤ q j + 1) ∧ (∀j<n. q j ≤ s j ∧ s j ≤ q j + 1) ∧ label r i ≠ label s i" proof - let ?rl = "reduced n ∘ label" let ?A = "{s. ksimplex p n s ∧ ?rl ` s = {..n}}" have "odd (card ?A)" using assms by (intro kuhn_combinatorial[of p n label]) auto then have "?A ≠ {}" by (rule odd_card_imp_not_empty) then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}" by (auto elim: ksimplex.cases) interpret kuhn_simplex p n b u s by fact show ?thesis proof (intro that[of b] allI impI) fix i assume "i < n" then show "b i < p" using base by auto next fix i assume "i < n" then have "i ∈ {.. n}" "Suc i ∈ {.. n}" by auto then obtain u v where u: "u ∈ s" "Suc i = ?rl u" and v: "v ∈ s" "i = ?rl v" unfolding rl[symmetric] by blast have "label u i ≠ label v i" using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"] u(2)[symmetric] v(2)[symmetric] ‹i < n› by auto moreover have "b j ≤ u j" "u j ≤ b j + 1" "b j ≤ v j" "v j ≤ b j + 1" if "j < n" for j using that base_le[OF ‹u∈s›] le_Suc_base[OF ‹u∈s›] base_le[OF ‹v∈s›] le_Suc_base[OF ‹v∈s›] by auto ultimately show "∃r s. (∀j<n. b j ≤ r j ∧ r j ≤ b j + 1) ∧ (∀j<n. b j ≤ s j ∧ s j ≤ b j + 1) ∧ label r i ≠ label s i" by blast qed qed subsubsection ‹Main result for the unit cube› lemma kuhn_labelling_lemma': assumes "(∀x::nat⇒real. P x ⟶ P (f x))" and "∀x. P x ⟶ (∀i::nat. Q i ⟶ 0 ≤ x i ∧ x i ≤ 1)" shows "∃l. (∀x i. l x i ≤ (1::nat)) ∧ (∀x i. P x ∧ Q i ∧ x i = 0 ⟶ l x i = 0) ∧ (∀x i. P x ∧ Q i ∧ x i = 1 ⟶ l x i = 1) ∧ (∀x i. P x ∧ Q i ∧ l x i = 0 ⟶ x i ≤ f x i) ∧ (∀x i. P x ∧ Q i ∧ l x i = 1 ⟶ f x i ≤ x i)" proof - have and_forall_thm: "⋀P Q. (∀x. P x) ∧ (∀x. Q x) ⟷ (∀x. P x ∧ Q x)" by auto have *: "∀x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ⟶ x ≠ 1 ∧ x ≤ y ∨ x ≠ 0 ∧ y ≤ x" by auto show ?thesis unfolding and_forall_thm apply (subst choice_iff[symmetric])+ apply rule apply rule proof - fix x x' let ?R = "λy::nat. (P x ∧ Q x' ∧ x x' = 0 ⟶ y = 0) ∧ (P x ∧ Q x' ∧ x x' = 1 ⟶ y = 1) ∧ (P x ∧ Q x' ∧ y = 0 ⟶ x x' ≤ (f x) x') ∧ (P x ∧ Q x' ∧ y = 1 ⟶ (f x) x' ≤ x x')" have "0 ≤ f x x' ∧ f x x' ≤ 1" if "P x" "Q x'" using assms(2)[rule_format,of "f x" x'] that apply (drule_tac assms(1)[rule_format]) apply auto done then have "?R 0 ∨ ?R 1" by auto then show "∃y≤1. ?R y" by auto qed qed subsection ‹Brouwer's fixed point theorem› text ‹We start proving Brouwer's fixed point theorem for the unit cube = ‹cbox 0 One›.› lemma brouwer_cube: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "continuous_on (cbox 0 One) f" and "f ` cbox 0 One ⊆ cbox 0 One" shows "∃x∈cbox 0 One. f x = x" proof (rule ccontr) define n where "n = DIM('a)" have n: "1 ≤ n" "0 < n" "n ≠ 0" unfolding n_def by (auto simp: Suc_le_eq DIM_positive) assume "¬ ?thesis" then have *: "¬ (∃x∈cbox 0 One. f x - x = 0)" by auto obtain d where d: "d > 0" "⋀x. x ∈ cbox 0 One ⟹ d ≤ norm (f x - x)" apply (rule brouwer_compactness_lemma[OF compact_cbox _ *]) apply (rule continuous_intros assms)+ apply blast done have *: "∀x. x ∈ cbox 0 One ⟶ f x ∈ cbox 0 One" "∀x. x ∈ (cbox 0 One::'a set) ⟶ (∀i∈Basis. True ⟶ 0 ≤ x ∙ i ∧ x ∙ i ≤ 1)" using assms(2)[unfolded image_subset_iff Ball_def] unfolding cbox_def by auto obtain label :: "'a ⇒ 'a ⇒ nat" where label [rule_format]: "∀x. ∀i∈Basis. label x i ≤ 1" "∀x. ∀i∈Basis. x ∈ cbox 0 One ∧ x ∙ i = 0 ⟶ label x i = 0" "∀x. ∀i∈Basis. x ∈ cbox 0 One ∧ x ∙ i = 1 ⟶ label x i = 1" "∀x. ∀i∈Basis. x ∈ cbox 0 One ∧ label x i = 0 ⟶ x ∙ i ≤ f x ∙ i" "∀x. ∀i∈Basis. x ∈ cbox 0 One ∧ label x i = 1 ⟶ f x ∙ i ≤ x ∙ i" using kuhn_labelling_lemma[OF *] by auto note label = this [rule_format] have lem1: "∀x∈cbox 0 One. ∀y∈cbox 0 One. ∀i∈Basis. label x i ≠ label y i ⟶ ¦f x ∙ i - x ∙ i¦ ≤ norm (f y - f x) + norm (y - x)" proof safe fix x y :: 'a assume x: "x ∈ cbox 0 One" and y: "y ∈ cbox 0 One" fix i assume i: "label x i ≠ label y i" "i ∈ Basis" have *: "⋀x y fx fy :: real. x ≤ fx ∧ fy ≤ y ∨ fx ≤ x ∧ y ≤ fy ⟹ ¦fx - x¦ ≤ ¦fy - fx¦ + ¦y - x¦" by auto have "¦(f x - x) ∙ i¦ ≤ ¦(f y - f x)∙i¦ + ¦(y - x)∙i¦" proof (cases "label x i = 0") case True then have fxy: "¬ f y ∙ i ≤ y ∙ i ⟹ f x ∙ i ≤ x ∙ i" by (metis True i label(1) label(5) le_antisym less_one not_le_imp_less y) show ?thesis unfolding inner_simps by (rule *) (auto simp: True i label x y fxy) next case False then show ?thesis using label [OF ‹i ∈ Basis›] i(1) x y apply (auto simp: inner_diff_left le_Suc_eq) by (metis "*") qed also have "… ≤ norm (f y - f x) + norm (y - x)" by (simp add: add_mono i(2) norm_bound_Basis_le) finally show "¦f x ∙ i - x ∙ i¦ ≤ norm (f y - f x) + norm (y - x)" unfolding inner_simps . qed have "∃e>0. ∀x∈cbox 0 One. ∀y∈cbox 0 One. ∀z∈cbox 0 One. ∀i∈Basis. norm (x - z) < e ⟶ norm (y - z) < e ⟶ label x i ≠ label y i ⟶ ¦(f(z) - z)∙i¦ < d / (real n)" proof - have d': "d / real n / 8 > 0" using d(1) by (simp add: n_def DIM_positive) have *: "uniformly_continuous_on (cbox 0 One) f" by (rule compact_uniformly_continuous[OF assms(1) compact_cbox]) obtain e where e: "e > 0" "⋀x x'. x ∈ cbox 0 One ⟹ x' ∈ cbox 0 One ⟹ norm (x' - x) < e ⟹ norm (f x' - f x) < d / real n / 8" using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] unfolding dist_norm by blast show ?thesis proof (intro exI conjI ballI impI) show "0 < min (e / 2) (d / real n / 8)" using d' e by auto fix x y z i assume as: "x ∈ cbox 0 One" "y ∈ cbox 0 One" "z ∈ cbox 0 One" "norm (x - z) < min (e / 2) (d / real n / 8)" "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i ≠ label y i" assume i: "i ∈ Basis" have *: "⋀z fz x fx n1 n2 n3 n4 d4 d :: real. ¦fx - x¦ ≤ n1 + n2 ⟹ ¦fx - fz¦ ≤ n3 ⟹ ¦x - z¦ ≤ n4 ⟹ n1 < d4 ⟹ n2 < 2 * d4 ⟹ n3 < d4 ⟹ n4 < d4 ⟹ (8 * d4 = d) ⟹ ¦fz - z¦ < d" by auto show "¦(f z - z) ∙ i¦ < d / real n" unfolding inner_simps proof (rule *) show "¦f x ∙ i - x ∙ i¦ ≤ norm (f y -f x) + norm (y - x)" using as(1) as(2) as(6) i lem1 by blast show "norm (f x - f z) < d / real n / 8" using d' e as by auto show "¦f x ∙ i - f z ∙ i¦ ≤ norm (f x - f z)" "¦x ∙ i - z ∙ i¦ ≤ norm (x - z)" unfolding inner_diff_left[symmetric] by (rule Basis_le_norm[OF i])+ have tria: "norm (y - x) ≤ norm (y - z) + norm (x - z)" using dist_triangle[of y x z, unfolded dist_norm] unfolding norm_minus_commute by auto also have "… < e / 2 + e / 2" using as(4) as(5) by auto finally show "norm (f y - f x) < d / real n / 8" using as(1) as(2) e(2) by auto have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8" using as(4) as(5) by auto with tria show "norm (y - x) < 2 * (d / real n / 8)" by auto qed (use as in auto) qed qed then obtain e where e: "e > 0" "⋀x y z i. x ∈ cbox 0 One ⟹ y ∈ cbox 0 One ⟹ z ∈ cbox 0 One ⟹ i ∈ Basis ⟹ norm (x - z) < e ∧ norm (y - z) < e ∧ label x i ≠ label y i ⟹ ¦(f z - z) ∙ i¦ < d / real n" by blast obtain p :: nat where p: "1 + real n / e ≤ real p" using real_arch_simple .. have "1 + real n / e > 0" using e(1) n by (simp add: add_pos_pos) then have "p > 0" using p by auto obtain b :: "nat ⇒ 'a" where b: "bij_betw b {..< n} Basis" by atomize_elim (auto simp: n_def intro!: finite_same_card_bij) define b' where "b' = inv_into {..< n} b" then have b': "bij_betw b' Basis {..< n}" using bij_betw_inv_into[OF b] by auto then have b'_Basis: "⋀i. i ∈ Basis ⟹ b' i ∈ {..< n}" unfolding bij_betw_def by (auto simp: set_eq_iff) have bb'[simp]:"⋀i. i ∈ Basis ⟹ b (b' i) = i" unfolding b'_def using b by (auto simp: f_inv_into_f bij_betw_def) have b'b[simp]:"⋀i. i < n ⟹ b' (b i) = i" unfolding b'_def using b by (auto simp: inv_into_f_eq bij_betw_def) have *: "⋀x :: nat. x = 0 ∨ x = 1 ⟷ x ≤ 1" by auto have b'': "⋀j. j < n ⟹ b j ∈ Basis" using b unfolding bij_betw_def by auto have q1: "0 < p" "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩_{R}i) ∘ b) i = 0 ∨ (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩_{R}i) ∘ b) i = 1)" unfolding * using ‹p > 0› ‹n > 0› using label(1)[OF b''] by auto { fix x :: "nat ⇒ nat" and i assume "∀i<n. x i ≤ p" "i < n" "x i = p ∨ x i = 0" then have "(∑i∈Basis. (real (x (b' i)) / real p) *⇩_{R}i) ∈ (cbox 0 One::'a set)" using b'_Basis by (auto simp: cbox_def inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) } note cube = this have q2: "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = 0 ⟶ (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩_{R}i) ∘ b) i = 0)" unfolding o_def using cube ‹p > 0› by (intro allI impI label(2)) (auto simp: b'') have q3: "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = p ⟶ (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩_{R}i) ∘ b) i = 1)" using cube ‹p > 0› unfolding o_def by (intro allI impI label(3)) (auto simp: b'') obtain q where q: "∀i<n. q i < p" "∀i<n. ∃r s. (∀j<n. q j ≤ r j ∧ r j ≤ q j + 1) ∧ (∀j<n. q j ≤ s j ∧ s j ≤ q j + 1) ∧ (label (∑i∈Basis. (real (r (b' i)) / real p) *⇩_{R}i) ∘ b) i ≠ (label (∑i∈Basis. (real (s (b' i)) / real p) *⇩_{R}i) ∘ b) i" by (rule kuhn_lemma[OF q1 q2 q3]) define z :: 'a where "z = (∑i∈Basis. (real (q (b' i)) / real p) *⇩_{R}i)" have "∃i∈Basis. d / real n ≤ ¦(f z - z)∙i¦" proof (rule ccontr) have "∀i∈Basis. q (b' i) ∈ {0..p}" using q(1) b' by (auto intro: less_imp_le simp: bij_betw_def) then have "z ∈ cbox 0 One" unfolding z_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) then have d_fz_z: "d ≤ norm (f z - z)" by (rule d) assume "¬ ?thesis" then have as: "∀i∈Basis. ¦f z ∙ i - z ∙ i¦ < d / real n" using ‹n > 0› by (auto simp: not_le inner_diff) have "norm (f z - z) ≤ (∑i∈Basis. ¦f z ∙ i - z ∙ i¦)" unfolding inner_diff_left[symmetric] by (rule norm_le_l1) also have "… < (∑(i::'a) ∈ Basis. d / real n)" by (meson as finite_Basis nonempty_Basis sum_strict_mono) also have "… = d" using DIM_positive[where 'a='a] by (auto simp: n_def) finally show False using d_fz_z by auto qed then obtain i where i: "i ∈ Basis" "d / real n ≤ ¦(f z - z) ∙ i¦" .. have *: "b' i < n" using i and b'[unfolded bij_betw_def] by auto obtain r s where rs: "⋀j. j < n ⟹ q j ≤ r j ∧ r j ≤ q j + 1" "⋀j. j < n ⟹ q j ≤ s j ∧ s j ≤ q j + 1" "(label (∑i∈Basis. (real (r (b' i)) / real p) *⇩_{R}i) ∘ b) (b' i) ≠ (label (∑i∈Basis. (real (s (b' i)) / real p) *⇩_{R}i) ∘ b) (b' i)" using q(2)[rule_format,OF *] by blast have b'_im: "⋀i. i ∈ Basis ⟹ b' i < n" using b' unfolding bij_betw_def by auto define r' ::'a where "r' = (∑i∈Basis. (real (r (b' i)) / real p) *⇩_{R}i)" have "⋀i. i ∈ Basis ⟹ r (b' i) ≤ p" apply (rule order_trans) apply (rule rs(1)[OF b'_im,THEN conjunct2]) using q(1)[rule_format,OF b'_im] apply (auto simp: Suc_le_eq) done then have "r' ∈ cbox 0 One" unfolding r'_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) define s' :: 'a where "s' = (∑i∈Basis. (real (s (b' i)) / real p) *⇩_{R}i)" have "⋀i. i ∈ Basis ⟹ s (b' i) ≤ p" using b'_im q(1) rs(2) by fastforce then have "s' ∈ cbox 0 One" unfolding s'_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) have "z ∈ cbox 0 One" unfolding z_def cbox_def using b'_Basis q(1)[rule_format,OF b'_im] ‹p > 0› by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le) { have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)" by (rule sum_mono) (use rs(1)[OF b'_im] in force) also have "… < e * real p" using p ‹e > 0› ‹p > 0› by (auto simp: field_simps n_def) finally have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) < e * real p" . } moreover { have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)" by (rule sum_mono) (use rs(2)[OF b'_im] in force) also have "… < e * real p" using p ‹e > 0› ‹p > 0› by (auto simp: field_simps n_def) finally have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) < e * real p" . } ultimately have "norm (r' - z) < e" and "norm (s' - z) < e" unfolding r'_def s'_def z_def using ‹p > 0› apply (rule_tac[!] le_less_trans[OF norm_le_l1]) apply (auto simp: field_simps sum_divide_distrib[symmetric] inner_diff_left) done then have "¦(f z - z) ∙ i¦ < d / real n" using rs(3) i unfolding r'_def[symmetric] s'_def[symmetric] o_def bb' by (intro e(2)[OF ‹r'∈cbox 0 One› ‹s'∈cbox 0 One› ‹z∈cbox 0 One›]) auto then show False using i by auto qed text ‹Next step is to prove it for nonempty interiors.› lemma brouwer_weak: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "compact S" and "convex S" and "interior S ≠ {}" and "continuous_on S f" and "f ` S ⊆ S" obtains x where "x ∈ S" and "f x = x" proof - let ?U = "cbox 0 One :: 'a set" have "∑Basis /⇩_{R}2 ∈ interior ?U" proof (rule interiorI) let ?I = "(⋂i∈Basis. {x::'a. 0 < x ∙ i} ∩ {x. x ∙ i < 1})" show "open ?I" by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id) show "∑Basis /⇩_{R}2 ∈ ?I" by simp show "?I ⊆ cbox 0 One" unfolding cbox_def by force qed then have *: "interior ?U ≠ {}" by fast have *: "?U homeomorphic S" using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] . have "∀f. continuous_on ?U f ∧ f ` ?U ⊆ ?U ⟶ (∃x∈?U. f x = x)" using brouwer_cube by auto then show ?thesis unfolding homeomorphic_fixpoint_property[OF *] using assms by (auto intro: that) qed text ‹Then the particular case for closed balls.› lemma brouwer_ball: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "e > 0" and "continuous_on (cball a e) f" and "f ` cball a e ⊆ cball a e" obtains x where "x ∈ cball a e" and "f x = x" using brouwer_weak[OF compact_cball convex_cball, of a e f] unfolding interior_cball ball_eq_empty using assms by auto text ‹And finally we prove Brouwer's fixed point theorem in its general version.› theorem brouwer: fixes f :: "'a::euclidean_space ⇒ 'a" assumes S: "compact S" "convex S" "S ≠ {}" and contf: "continuous_on S f" and fim: "f ` S ⊆ S" obtains x where "x ∈ S" and "f x = x" proof - have "∃e>0. S ⊆ cball 0 e" using compact_imp_bounded[OF ‹compact S›] unfolding bounded_pos by auto then obtain e where e: "e > 0" "S ⊆ cball 0 e" by blast have "∃x∈ cball 0 e. (f ∘ closest_point S) x = x" proof (rule_tac brouwer_ball[OF e(1)]) show "continuous_on (cball 0 e) (f ∘ closest_point S)" apply (rule continuous_on_compose) using S compact_eq_bounded_closed continuous_on_closest_point apply blast by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI) show "(f ∘ closest_point S) ` cball 0 e ⊆ cball 0 e" by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE) qed (use assms in auto) then obtain x where x: "x ∈ cball 0 e" "(f ∘ closest_point S) x = x" .. have "x ∈ S" by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2)) then have *: "closest_point S x = x" by (rule closest_point_self) show thesis proof show "closest_point S x ∈ S" by (simp add: "*" ‹x ∈ S›) show "f (closest_point S x) = closest_point S x" using "*" x(2) by auto qed qed subsection ‹Applications› text ‹So we get the no-retraction theorem.› corollary no_retraction_cball: fixes a :: "'a::euclidean_space" assumes "e > 0" shows "¬ (frontier (cball a e) retract_of (cball a e))" proof assume *: "frontier (cball a e) retract_of (cball a e)" have **: "⋀xa. a - (2 *⇩_{R}a - xa) = - (a - xa)" using scaleR_left_distrib[of 1 1 a] by auto obtain x where x: "x ∈ {x. norm (a - x) = e}" "2 *⇩_{R}a - x = x" proof (rule retract_fixpoint_property[OF *, of "λx. scaleR 2 a - x"]) show "continuous_on (frontier (cball a e)) ((-) (2 *⇩_{R}a))" by (intro continuous_intros) show "(-) (2 *⇩_{R}a) ` frontier (cball a e) ⊆ frontier (cball a e)" by clarsimp (metis "**" dist_norm norm_minus_cancel) qed (auto simp: dist_norm intro: brouwer_ball[OF assms]) then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp: algebra_simps) then have "a = x" unfolding scaleR_left_distrib[symmetric] by auto then show False using x assms by auto qed corollary contractible_sphere: fixes a :: "'a::euclidean_space" shows "contractible(sphere a r) ⟷ r ≤ 0" proof (cases "0 < r") case True then show ?thesis unfolding contractible_def nullhomotopic_from_sphere_extension using no_retraction_cball [OF True, of a] by (auto simp: retract_of_def retraction_def) next case False then show ?thesis unfolding contractible_def nullhomotopic_from_sphere_extension using continuous_on_const less_eq_real_def by auto qed corollary connected_sphere_eq: fixes a :: "'a :: euclidean_space" shows "connected(sphere a r) ⟷ 2 ≤ DIM('a) ∨ r ≤ 0" (is "?lhs = ?rhs") proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis by auto next case equal then show ?thesis by auto next case greater show ?thesis proof assume L: ?lhs have "False" if 1: "DIM('a) = 1" proof - obtain x y where xy: "sphere a r = {x,y}" "x ≠ y" using sphere_1D_doubleton [OF 1 greater] by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist) then have "finite (sphere a r)" by auto with L ‹r > 0› xy show "False" using connected_finite_iff_sing by auto qed with greater show ?rhs by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq) next assume ?rhs then show ?lhs using connected_sphere greater by auto qed qed corollary path_connected_sphere_eq: fixes a :: "'a :: euclidean_space" shows "path_connected(sphere a r) ⟷ 2 ≤ DIM('a) ∨ r ≤ 0" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using connected_sphere_eq path_connected_imp_connected by blast next assume R: ?rhs then show ?lhs by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere) qed proposition frontier_subset_retraction: fixes S :: "'a::euclidean_space set" assumes "bounded S" and fros: "frontier S ⊆ T" and contf: "continuous_on (closure S) f" and fim: "f ` S ⊆ T" and fid: "⋀x. x ∈ T ⟹ f x = x" shows "S ⊆ T" proof (rule ccontr) assume "¬ S ⊆ T" then obtain a where "a ∈ S" "a ∉ T" by blast define g where "g ≡ λz. if z ∈ closure S then f z else z" have "continuous_on (closure S ∪ closure(-S)) g" unfolding g_def apply (rule continuous_on_cases) using fros fid frontier_closures apply (auto simp: contf continuous_on_id) done moreover have "closure S ∪ closure(- S) = UNIV" using closure_Un by fastforce ultimately have contg: "continuous_on UNIV g" by metis obtain B where "0 < B" and B: "closure S ⊆ ball a B" using ‹bounded S› bounded_subset_ballD by blast have notga: "g x ≠ a" for x unfolding g_def using fros fim ‹a ∉ T› apply (auto simp: frontier_def) using fid interior_subset apply fastforce by (simp add: ‹a ∈ S› closure_def) define h where "h ≡ (λy. a + (B / norm(y - a)) *⇩_{R}(y - a)) ∘ g" have "¬ (frontier (cball a B) retract_of (cball a B))" by (metis no_retraction_cball ‹0 < B›) then have "⋀k. ¬ retraction (cball a B) (frontier (cball a B)) k" by (simp add: retract_of_def) moreover have "retraction (cball a B) (frontier (cball a B)) h" unfolding retraction_def proof (intro conjI ballI) show "frontier (cball a B) ⊆ cball a B" by force show "continuous_on (cball a B) h" unfolding h_def by (intro continuous_intros) (use contg continuous_on_subset notga in auto) show "h ` cball a B ⊆ frontier (cball a B)" using ‹0 < B› by (auto simp: h_def notga dist_norm) show "⋀x. x ∈ frontier (cball a B) ⟹ h x = x" apply (auto simp: h_def algebra_simps) apply (simp add: vector_add_divide_simps notga) by (metis (no_types, hide_lams) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq) qed ultimately show False by simp qed subsubsection ‹Punctured affine hulls, etc› lemma rel_frontier_deformation_retract_of_punctured_convex: fixes S :: "'a::euclidean_space set" assumes "convex S" "convex T" "bounded S" and arelS: "a ∈ rel_interior S" and relS: "rel_frontier S ⊆ T" and affS: "T ⊆ affine hull S" obtains r where "homotopic_with_canon (λx. True) (T - {a}) (T - {a}) id r" "retraction (T - {a}) (rel_frontier S) r" proof - have "∃d. 0 < d ∧ (a + d *⇩_{R}l) ∈ rel_frontier S ∧ (∀e. 0 ≤ e ∧ e < d ⟶ (a + e *⇩_{R}l) ∈ rel_interior S)" if "(a + l) ∈ affine hull S" "l ≠ 0" for l apply (rule ray_to_rel_frontier [OF ‹bounded S› arelS]) apply (rule that)+ by metis then obtain dd where dd1: "⋀l. ⟦(a + l) ∈ affine hull S; l ≠ 0⟧ ⟹ 0 < dd l ∧ (a + dd l *⇩_{R}l) ∈ rel_frontier S" and dd2: "⋀l e. ⟦(a + l) ∈ affine hull S; e < dd l; 0 ≤ e; l ≠ 0⟧ ⟹ (a + e *⇩_{R}l) ∈ rel_interior S" by metis+ have aaffS: "a ∈ affine hull S" by (meson arelS subsetD hull_inc rel_interior_subset) have "((λz. z - a) ` (affine hull S - {a})) = ((λz. z - a) ` (affine hull S)) - {0}" by auto moreover have "continuous_on (((λz. z - a) ` (affine hull S)) - {0}) (λx. dd x *⇩_{R}x)" proof (rule continuous_on_compact_surface_projection) show "compact (rel_frontier ((λz. z - a) ` S))" by (simp add: ‹bounded S› bounded_translation_minus compact_rel_frontier_bounded) have releq: "rel_frontier ((λz. z - a) ` S) = (λz. z - a) ` rel_frontier S" using rel_frontier_translation [of "-a"] add.commute by simp also have "… ⊆ (λz. z - a) ` (affine hull S) - {0}" using rel_frontier_affine_hull arelS rel_frontier_def by fastforce finally show "rel_frontier ((λz. z - a) ` S) ⊆ (λz. z - a) ` (affine hull S) - {0}" . show "cone ((λz. z - a) ` (affine hull S))" by (rule subspace_imp_cone) (use aaffS in ‹simp add: subspace_affine image_comp o_def affine_translation_aux [of a]›) show "(0 < k ∧ k *⇩_{R}x ∈ rel_frontier ((λz. z - a) ` S)) ⟷ (dd x = k)" if x: "x ∈ (λz. z - a) ` (affine hull S) - {0}" for k x proof show "dd x = k ⟹ 0 < k ∧ k *⇩_{R}x ∈ rel_frontier ((λz. z - a) ` S)" using dd1 [of x] that image_iff by (fastforce simp add: releq) next assume k: "0 < k ∧ k *⇩_{R}x ∈ rel_frontier ((λz. z - a) ` S)" have False if "dd x < k" proof - have "k ≠ 0" "a + k *⇩_{R}x ∈ closure S" using k closure_translation [of "-a"] by (auto simp: rel_frontier_def cong: image_cong_simp) then have segsub: "open_segment a (a + k *⇩_{R}x) ⊆ rel_interior S" by (metis rel_interior_closure_convex_segment [OF ‹convex S› arelS]) have "x ≠ 0" and xaffS: "a + x ∈ affine hull S" using x by auto then have "0 < dd x" and inS: "a + dd x *⇩_{R}x ∈ rel_frontier S" using dd1 by auto moreover have "a + dd x *⇩_{R}x ∈ open_segment a (a + k *⇩_{R}x)" using k ‹x ≠ 0› ‹0 < dd x› apply (simp add: in_segment) apply (rule_tac x = "dd x / k" in exI) apply (simp add: field_simps that) apply (simp add: vector_add_divide_simps algebra_simps) apply (metis (no_types) ‹k ≠ 0› divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse) done ultimately show ?thesis using segsub by (auto simp: rel_frontier_def) qed moreover have False if "k < dd x" using x k that rel_frontier_def by (fastforce simp: algebra_simps releq dest!: dd2) ultimately show "dd x = k" by fastforce qed qed ultimately have *: "continuous_on ((λz. z - a) ` (affine hull S - {a})) (λx. dd x *⇩_{R}x)" by auto have "continuous_on (affine hull S - {a}) ((λx. a + dd x *⇩_{R}x) ∘ (λz. z - a))" by (intro * continuous_intros continuous_on_compose) with affS have contdd: "continuous_on (T - {a}) ((λx. a + dd x *⇩_{R}x) ∘ (λz. z - a))" by (blast intro: continuous_on_subset) show ?thesis proof show "homotopic_with_canon (λx. True) (T - {a}) (T - {a}) id (λx. a + dd (x - a) *⇩_{R}(x - a))" proof (rule homotopic_with_linear) show "continuous_on (T - {a}) id" by (intro continuous_intros continuous_on_compose) show "continuous_on (T - {a}) (λx. a + dd (x - a) *⇩_{R}(x - a))" using contdd by (simp add: o_def) show "closed_segment (id x) (a + dd (x - a) *⇩_{R}(x - a)) ⊆ T - {a}" if "x ∈ T - {a}" for x proof (clarsimp simp: in_segment, intro conjI) fix u::real assume u: "0 ≤ u" "u ≤ 1" have "a + dd (x - a) *⇩_{R}(x - a) ∈ T" by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that) then show "(1 - u) *⇩_{R}x + u *⇩_{R}(a + dd (x - a) *⇩_{R}(x - a)) ∈ T" using convexD [OF ‹convex T›] that u by simp have iff: "(1 - u) *⇩_{R}x + u *⇩_{R}(a + d *⇩_{R}(x - a)) = a ⟷ (1 - u + u * d) *⇩_{R}(x - a) = 0" for d by (auto simp: algebra_simps) have "x ∈ T" "x ≠ a" using that by auto then have axa: "a + (x - a) ∈ affine hull S" by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD) then have "¬ dd (x - a) ≤ 0 ∧ a + dd (x - a) *⇩_{R}(x - a) ∈ rel_frontier S" using ‹x ≠ a› dd1 by fastforce with ‹x ≠ a› show "(1 - u) *⇩_{R}x + u *⇩_{R}(a + dd (x - a) *⇩_{R}(x - a)) ≠ a" apply (auto simp: iff) using less_eq_real_def mult_le_0_iff not_less u by fastforce qed qed show "retraction (T - {a}) (rel_frontier S) (λx. a + dd (x - a) *⇩_{R}(x - a))" proof (simp add: retraction_def, intro conjI ballI) show "rel_frontier S ⊆ T - {a}" using arelS relS rel_frontier_def by fastforce show "continuous_on (T - {a}) (λx. a + dd (x - a) *⇩_{R}(x - a))" using contdd by (simp add: o_def) show "(λx. a + dd (x - a) *⇩_{R}(x - a)) ` (T - {a}) ⊆ rel_frontier S" apply (auto simp: rel_frontier_def) apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff) by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD) show "a + dd (x - a) *⇩_{R}(x - a) = x" if x: "x ∈ rel_frontier S" for x proof - have "x ≠ a" using that arelS by (auto simp: rel_frontier_def) have False if "dd (x - a) < 1" proof - have "x ∈ closure S" using x by (auto simp: rel_frontier_def) then have segsub: "open_segment a x ⊆ rel_interior S" by (metis rel_interior_closure_convex_segment [OF ‹convex S› arelS]) have xaffS: "x ∈ affine hull S" using affS relS x by auto then have "0 < dd (x - a)" and inS: "a + dd (x - a) *⇩_{R}(x - a) ∈ rel_frontier S" using dd1 by (auto simp: ‹x ≠ a›) moreover have "a + dd (x - a) *⇩_{R}(x - a) ∈ open_segment a x" using ‹x ≠ a› ‹0 < dd (x - a)› apply (simp add: in_segment) apply (rule_tac x = "dd (x - a)" in exI) apply (simp add: algebra_simps that) done ultimately show ?thesis using segsub by (auto simp: rel_frontier_def) qed moreover have False if "1 < dd (x - a)" using x that dd2 [of "x - a" 1] ‹x ≠ a› closure_affine_hull by (auto simp: rel_frontier_def) ultimately have