(* Author: John Harrison
Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
*)
(* ========================================================================= *)
(* Results connected with topological dimension. *)
(* *)
(* 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 \<open>Results connected with topological dimension.\<close>
theory Brouwer_Fixpoint
imports Path_Connected Homeomorphism
begin
lemma bij_betw_singleton_eq:
assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> 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 Diff_subset)
moreover have "f a \<in> B" "g a \<in> 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 \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
apply (auto simp: Fun.swap_def image_iff)
apply metis
apply (metis member_remove remove_def)
apply (metis member_remove remove_def)
done
lemmas swap_apply1 = swap_apply(1)
lemmas swap_apply2 = swap_apply(2)
lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
lemmas Zero_notin_Suc = zero_notin_Suc_image
lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
lemma setsum_union_disjoint':
assumes "finite A"
and "finite B"
and "A \<inter> B = {}"
and "A \<union> B = C"
shows "setsum g C = setsum g A + setsum g B"
using setsum.union_disjoint[OF assms(1-3)] and assms(4) by auto
lemma pointwise_minimal_pointwise_maximal:
fixes s :: "(nat \<Rightarrow> nat) set"
assumes "finite s"
and "s \<noteq> {}"
and "\<forall>x\<in>s. \<forall>y\<in>s. x \<le> y \<or> y \<le> x"
shows "\<exists>a\<in>s. \<forall>x\<in>s. a \<le> x"
and "\<exists>a\<in>s. \<forall>x\<in>s. x \<le> a"
using assms
proof (induct s rule: finite_ne_induct)
case (insert b s)
assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
using insert by auto
with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
qed auto
lemma brouwer_compactness_lemma:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "compact s"
and "continuous_on s f"
and "\<not> (\<exists>x\<in>s. f x = 0)"
obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
proof (cases "s = {}")
case True
show thesis
by (rule that [of 1]) (auto simp: True)
next
case False
have "continuous_on s (norm \<circ> f)"
by (rule continuous_intros continuous_on_norm assms(2))+
with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
unfolding o_def
by auto
have "(norm \<circ> f) x > 0"
using assms(3) and x(1)
by auto
then show ?thesis
by (rule that) (insert x(2), auto simp: o_def)
qed
lemma kuhn_labelling_lemma:
fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
assumes "\<forall>x. P x \<longrightarrow> P (f x)"
and "\<forall>x. P x \<longrightarrow> (\<forall>i\<in>Basis. Q i \<longrightarrow> 0 \<le> x\<bullet>i \<and> x\<bullet>i \<le> 1)"
shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f x\<bullet>i) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f x\<bullet>i \<le> x\<bullet>i)"
proof -
{ fix x i
let ?R = "\<lambda>y. (P x \<and> Q i \<and> x \<bullet> i = 0 \<longrightarrow> y = (0::nat)) \<and>
(P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
(P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
(P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
{ assume "P x" "Q i" "i \<in> Basis" with assms have "0 \<le> f x \<bullet> i \<and> f x \<bullet> i \<le> 1" by auto }
then have "i \<in> Basis \<Longrightarrow> ?R 0 \<or> ?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
subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
lemma kuhn_counting_lemma:
fixes bnd compo compo' face S F
defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
assumes [simp, intro]: "finite F" \<comment> "faces" and [simp, intro]: "finite S" \<comment> "simplices"
and "\<And>f. f \<in> F \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 1"
and "\<And>f. f \<in> F \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 2"
and "\<And>s. s \<in> S \<Longrightarrow> compo s \<Longrightarrow> nF s = 1"
and "\<And>s. s \<in> S \<Longrightarrow> \<not> compo s \<Longrightarrow> nF s = 0 \<or> nF s = 2"
and "odd (card {f\<in>F. compo' f \<and> bnd f})"
shows "odd (card {s\<in>S. compo s})"
proof -
have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + (\<Sum>s | s \<in> S \<and> compo s. nF s) = (\<Sum>s\<in>S. nF s)"
by (subst setsum.union_disjoint[symmetric]) (auto intro!: setsum.cong)
also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
(\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
unfolding setsum.distrib[symmetric]
by (subst card_Un_disjoint[symmetric])
(auto simp: nF_def intro!: setsum.cong arg_cong[where f=card])
also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount)
finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
using assms(6,8) by simp
moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
(\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
using assms(7) by (subst setsum.union_disjoint[symmetric]) (fastforce intro!: setsum.cong)+
ultimately show ?thesis
by auto
qed
subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
lemma kuhn_complete_lemma:
assumes [simp]: "finite simplices"
and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
and card_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"
and rl_bd: "\<And>s. s \<in> simplices \<Longrightarrow> rl ` s \<subseteq> {..Suc n}"
and bnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 1"
and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2"
and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})"
shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
let ?F = "{f. \<exists>s\<in>simplices. face f s}"
have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
by (auto simp: face)
show "finite ?F"
using \<open>finite simplices\<close> unfolding F_eq by auto
show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
using bnd that by auto
show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
using nbnd that by auto
show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
using odd_card by simp
fix s assume s[simp]: "s \<in> simplices"
let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {..n}}"
have "?S = (\<lambda>a. s - {a}) ` {a\<in>s. rl ` (s - {a}) = {..n}}"
using s by (fastforce simp: face)
then have card_S: "card ?S = card {a\<in>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 \<in> s"
by (metis atMost_iff image_iff le_Suc_eq rl)
ultimately have n: "{..n} = rl ` (s - {a})"
by (auto simp add: inj_on_image_set_diff Diff_subset rl)
have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
using inj_rl \<open>a \<in> s\<close> by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
then show "card ?S = 1"
unfolding card_S by simp }
{ assume rl: "rl ` s \<noteq> {..Suc n}"
show "card ?S = 0 \<or> card ?S = 2"
proof cases
assume *: "{..n} \<subseteq> rl ` s"
with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
then have "\<not> inj_on rl s"
by (intro pigeonhole) simp
then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> 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 add: rl_s card_Diff_singleton_if)
{ fix x assume "x \<in> s" "x \<notin> {a, b}"
then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
also have "\<dots> = rl ` (s - {x})"
using ab \<open>x \<notin> {a, b}\<close> by auto
also assume "\<dots> = rl ` s"
finally have False
using \<open>x\<in>s\<close> by auto }
moreover
{ fix x assume "x \<in> {a, b}" with ab have "x \<in> s \<and> rl ` (s - {x}) = rl ` s"
by (simp add: set_eq_iff image_iff Bex_def) metis }
ultimately have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a, b}"
unfolding rl_s[symmetric] by fastforce
with \<open>a \<noteq> b\<close> show "card ?S = 0 \<or> card ?S = 2"
unfolding card_S by simp
next
assume "\<not> {..n} \<subseteq> rl ` s"
then have "\<And>x. rl ` (s - {x}) \<noteq> {..n}"
by auto
then show "card ?S = 0 \<or> card ?S = 2"
unfolding card_S by simp
qed }
qed fact
locale kuhn_simplex =
fixes p n and base upd and s :: "(nat \<Rightarrow> nat) set"
assumes base: "base \<in> {..< n} \<rightarrow> {..< p}"
assumes base_out: "\<And>i. n \<le> i \<Longrightarrow> base i = p"
assumes upd: "bij_betw upd {..< n} {..< n}"
assumes s_pre: "s = (\<lambda>i j. if j \<in> upd`{..< i} then Suc (base j) else base j) ` {.. n}"
begin
definition "enum i j = (if j \<in> 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 \<Longrightarrow> upd i < n"
using upd by (auto dest!: bij_betwE)
lemma s_space: "s \<subseteq> {..< n} \<rightarrow> {.. p}"
proof -
{ fix i assume "i \<le> n" then have "enum i \<in> {..< n} \<rightarrow> {.. 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 \<noteq> y" "x \<le> n" "y \<le> n"
with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
then have "enum x \<noteq> enum y"
by (auto simp add: 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 \<in> s"
unfolding s_eq by (subst enum_0[symmetric]) auto
lemma enum_in: "i \<le> n \<Longrightarrow> enum i \<in> s"
unfolding s_eq by auto
lemma one_step:
assumes a: "a \<in> s" "j < n"
assumes *: "\<And>a'. a' \<in> s \<Longrightarrow> a' \<noteq> a \<Longrightarrow> a' j = p'"
shows "a j \<noteq> p'"
proof
assume "a j = p'"
with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
by auto
then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
unfolding s_eq by auto
from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
by (auto simp: enum_def fun_eq_iff split: if_split_asm)
with upd \<open>j < n\<close> show False
by (auto simp: bij_betw_def)
qed
lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> 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 \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
using inj_on_image_mem_iff[of upd "{..< n}"] upd
by (auto simp: bij_betw_def)
lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
using inj_enum by (auto simp: inj_on_eq_iff)
lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
using inj_on_image_mem_iff[OF inj_enum] by auto
lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
by (auto simp: s_eq enum_mono)
lemma less: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a i < b i \<Longrightarrow> a < b"
using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
lemma enum_0_bot: "a \<in> s \<Longrightarrow> a = enum 0 \<longleftrightarrow> (\<forall>a'\<in>s. a \<le> a')"
unfolding s_eq by (auto simp: enum_mono Ball_def)
lemma enum_n_top: "a \<in> s \<Longrightarrow> a = enum n \<longleftrightarrow> (\<forall>a'\<in>s. a' \<le> a)"
unfolding s_eq by (auto simp: enum_mono Ball_def)
lemma enum_Suc: "i < n \<Longrightarrow> 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 \<le> n \<Longrightarrow> n \<le> j \<Longrightarrow> 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 \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
unfolding s_eq by (auto simp add: enum_eq_p)
lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
using out_eq_p[of a j] s_space by (cases "j < n") auto
lemma le_Suc_base: "a \<in> s \<Longrightarrow> a j \<le> Suc (base j)"
unfolding s_eq by (auto simp: enum_def)
lemma base_le: "a \<in> s \<Longrightarrow> base j \<le> a j"
unfolding s_eq by (auto simp: enum_def)
lemma enum_le_p: "i \<le> n \<Longrightarrow> j < n \<Longrightarrow> enum i j \<le> p"
using enum_in[of i] s_space by auto
lemma enum_less: "a \<in> s \<Longrightarrow> i < n \<Longrightarrow> enum i < a \<longleftrightarrow> enum (Suc i) \<le> a"
unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
lemma ksimplex_0:
"n = 0 \<Longrightarrow> s = {(\<lambda>x. p)}"
using s_eq enum_def base_out by auto
lemma replace_0:
assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = 0" and "x \<in> s"
shows "x \<le> a"
proof cases
assume "x \<noteq> a"
have "a j \<noteq> 0"
using assms by (intro one_step[where a=a]) auto
with less[OF \<open>x\<in>s\<close> \<open>a\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
show ?thesis
by auto
qed simp
lemma replace_1:
assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = p" and "x \<in> s"
shows "a \<le> x"
proof cases
assume "x \<noteq> a"
have "a j \<noteq> p"
using assms by (intro one_step[where a=a]) auto
with enum_le_p[of _ j] \<open>j < n\<close> \<open>a\<in>s\<close>
have "a j < p"
by (auto simp: less_le s_eq)
with less[OF \<open>a\<in>s\<close> \<open>x\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
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 \<le> l" "l \<le> j" and "j + d \<le> 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 \<in> t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \<in> s.enum ` {i .. j}"
using eq by auto
from t \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "s.enum i \<le> t.enum (i + d)"
by (auto simp: s.enum_mono)
moreover from s \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "t.enum (i + d) \<le> s.enum i"
by (auto simp: t.enum_mono)
ultimately show ?case
by auto
next
case (step l)
moreover from step.prems \<open>j + d \<le> n\<close> 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) \<in> t.enum ` {i + d .. j + d}"
"t.enum (Suc l + d) \<in> s.enum ` {i .. j}"
using step \<open>j + d \<le> n\<close> eq by (auto simp: s.enum_inj t.enum_inj)
ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
using \<open>j + d \<le> n\<close>
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 \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a \<le> a'"
assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b \<le> 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 \<noteq> 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 \<open>n \<noteq> 0\<close> 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 \<le> 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 \<open>n \<noteq> 0\<close> 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 "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
by (auto simp: gr0_conv_Suc)
with \<open>n \<noteq> 0\<close> 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 \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a' \<le> a"
assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b' \<le> 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 "\<And>j. j < n' \<Longrightarrow> 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 \<Longrightarrow> 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 \<in> 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 \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>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} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>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" "\<forall>x\<in>s'. x n = p"
shows "ksimplex p n s' \<longleftrightarrow> (\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a})"
using assms
proof safe
fix s a assume "ksimplex p (Suc n) s" and a: "a \<in> s" and na: "\<forall>x\<in>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 \<open>a\<in>s\<close> s_space by (auto simp: less_le)
then have "a = enum 0"
using \<open>a \<in> s\<close> 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 in_enum_image subset_eq)
then have "enum 1 \<in> s - {a}"
by auto
then have "upd 0 = n"
using \<open>a n < p\<close> \<open>a = enum 0\<close> 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\<circ>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 \<open>enum 1 \<in> s - {a}\<close>] \<open>a = enum 0\<close> by (auto simp: \<open>upd 0 = n\<close>)
show ?thesis
proof (rule ksimplex.intros, standard)
show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
using base base_out by (auto simp: Pi_iff)
have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
by (auto simp: image_iff Ball_def) arith
then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
using \<open>upd 0 = n\<close> upd_inj
by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
using \<open>upd 0 = n\<close> by auto
define f' where "f' i j =
(if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
{ fix x i assume i[arith]: "i \<le> n" then have "enum (Suc i) x = f' i x"
unfolding f'_def enum_def using \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
by (simp add: upd_Suc enum_0 n_in_upd) }
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 *: "\<forall>x\<in>s'. x n = p"
then show "\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> 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 \<Rightarrow> n | Suc i \<Rightarrow> upd i)" for i
have "ksimplex p (Suc n) (s' \<union> {b})"
proof (rule ksimplex.intros, standard)
show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
using base_out by (auto simp: b_def)
have "bij_betw u (Suc ` {..< n} \<union> {0}) ({..<n} \<union> {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 \<in> u`{..< i} then Suc (b j) else b j)" for i j
have u_eq: "\<And>i. i \<le> n \<Longrightarrow> u ` {..< Suc i} = upd ` {..< i} \<union> { n }"
by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
{ fix x have "x \<le> n \<Longrightarrow> n \<notin> upd ` {..<x}"
using upd_space by (simp add: image_iff neq_iff) }
note n_not_upd = this
have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \<union> {0})"
unfolding atMost_Suc_eq_insert_0 by simp
also have "\<dots> = (f' \<circ> Suc) ` {.. n} \<union> {b}"
by (auto simp: f'_def)
also have "(f' \<circ> Suc) ` {.. n} = s'"
using \<open>0 < p\<close> 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' \<union> {b} = f' ` {.. Suc n}" ..
qed
moreover have "b \<notin> s'"
using * \<open>0 < p\<close> 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 \<in> s"
assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = 0"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>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 \<in> 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' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
using s \<open>a \<in> s\<close> by auto
then show ?thesis
by simp
qed
lemma ksimplex_replace_1:
assumes s: "ksimplex p n s" and a: "a \<in> s"
assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = p"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>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 \<in> 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' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
using s \<open>a \<in> s\<close> by auto
then show ?thesis
by simp
qed
lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
by (auto simp add: card_Suc_eq eval_nat_numeral)
lemma ksimplex_replace_2:
assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
and ub: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> p"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
using s
proof cases
case (ksimplex base upd)
then interpret kuhn_simplex p n base upd s .
from \<open>a \<in> s\<close> obtain i where "i \<le> n" "a = enum i"
unfolding s_eq by auto
from \<open>i \<le> n\<close> have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
by linarith
then have "\<exists>!s'. s' \<noteq> s \<and> ksimplex p n s' \<and> (\<exists>b\<in>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 \<circ> 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 \<in> ?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 \<circ> rot" "f' ` {.. n}"
proof
from \<open>a = enum i\<close> ub \<open>n \<noteq> 0\<close> \<open>i = 0\<close>
obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
unfolding s_eq by (auto intro: upd_space simp: enum_inj)
then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
then have "enum 1 (upd 0) < p"
by (auto simp add: le_fun_def intro: le_less_trans)
then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
using base \<open>n \<noteq> 0\<close> by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
{ fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
using \<open>n \<noteq> 0\<close> 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 [simp]: "\<And>j. j < n \<Longrightarrow> rot ` {..< j} = {0 <..< Suc j}"
by (auto simp: rot_def image_iff Ball_def)
arith
{ fix j assume j: "j < n"
from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
note f'_eq_enum = this
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 \<open>a = enum i\<close> \<open>i = 0\<close>
by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
have "enum 0 < f' 0"
using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
also have "\<dots> < f' n"
using \<open>n \<noteq> 0\<close> b.enum_strict_mono[of 0 n] unfolding b_enum by simp
finally have "a \<noteq> f' n"
using \<open>a = enum i\<close> \<open>i = 0\<close> by auto
{ fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
obtain b u where "kuhn_simplex p n b u t"
using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b u t .
{ fix x assume "x \<in> s" "x \<noteq> a"
then have "x (upd 0) = enum (Suc 0) (upd 0)"
by (auto simp: \<open>a = enum i\<close> \<open>i = 0\<close> s_eq enum_def enum_inj) }
then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
unfolding eq_sma[symmetric] by auto
then have "c (upd 0) \<noteq> enum (Suc 0) (upd 0)"
using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: upd_space)
then have "c (upd 0) < enum (Suc 0) (upd 0) \<or> c (upd 0) > enum (Suc 0) (upd 0)"
by auto
then have "t = s \<or> 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 \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
note top = this
have "s = t"
using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
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 \<circ> rot" "f' ` {.. n}" b u t ..
have eq: "f' ` {..n} - {f' n} = t - {c}"
using eq_sma eq by simp
{ fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
note top = this
have "f' ` {..n} = t"
using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
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 \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
apply (intro ex1I[of _ "f' ` {.. n}"])
apply auto []
apply metis
done
next
assume "i = n"
from \<open>n \<noteq> 0\<close> obtain n' where n': "n = Suc n'"
by (cases n) auto
define rot where "rot i = (case i of 0 \<Rightarrow> n' | Suc i \<Rightarrow> i)" for i
let ?upd = "upd \<circ> 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 \<in> ?upd`{..< i} then Suc (b j) else b j)" for i j
interpret b: kuhn_simplex p n b "upd \<circ> rot" "f' ` {.. n}"
proof
{ fix i assume "n \<le> i" then show "b i = p"
using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
show "b \<in> {..<n} \<rightarrow> {..<p}"
using base \<open>n \<noteq> 0\<close> 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 \<open>n \<noteq> 0\<close> by auto
{ from \<open>a = enum i\<close> \<open>n \<noteq> 0\<close> \<open>i = n\<close> lb upd_space[of n']
obtain i' where "i' \<le> n" "enum i' \<noteq> 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 \<open>i' \<le> n\<close> \<open>enum i' \<noteq> enum n\<close> 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 \<open>0<n\<close>] b.enum_0 by (auto simp: b_def rot_def)
have [simp]: "\<And>j. Suc j < n \<Longrightarrow> rot ` {..< Suc j} = {n'} \<union> {..< j}"
by (auto simp: rot_def image_iff Ball_def split: nat.splits)
have rot_simps: "\<And>j. rot (Suc j) = j" "rot 0 = n'"
by (simp_all add: rot_def)
{ fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
by (induct j) (auto simp add: 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 add: 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 \<open>a = enum i\<close> \<open>i = n\<close>
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 \<le> b.enum n"
by (simp add: b.enum_mono)
also have "b.enum n < enum n"
using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono b_enum_eq_enum n')
finally have "a \<noteq> b.enum 0"
using \<open>a = enum i\<close> \<open>i = n\<close> by auto
{ fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
obtain b' u where "kuhn_simplex p n b' u t"
using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b' u t .
{ fix x assume "x \<in> s" "x \<noteq> a"
then have "x (upd n') = enum n' (upd n')"
by (auto simp: \<open>a = enum i\<close> n' \<open>i = n\<close> s_eq enum_def enum_inj in_upd_image) }
then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd n') = enum n' (upd n')"
unfolding eq_sma[symmetric] by auto
then have "c (upd n') \<noteq> enum n' (upd n')"
using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: n' upd_space[unfolded n'])
then have "c (upd n') < enum n' (upd n') \<or> c (upd n') > enum n' (upd n')"
by auto
then have "t = s \<or> 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 \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
note top = this
have "s = t"
using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
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 \<circ> 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 \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
note bot = this
have "f' ` {..n} = t"
using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
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 \<open>a \<noteq> b.enum 0\<close> \<open>n \<noteq> 0\<close> 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 \<in> ?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 \<in> {..<n} \<rightarrow> {..<p}" by fact
{ fix i assume "n \<le> i" then show "base i = p" by fact }
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} \<subseteq> {..n}"
using i by auto
{ fix j assume "j \<le> n"
moreover have "j < i \<or> i = j \<or> i < j" by arith
moreover note i
ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
unfolding enum_def[abs_def] b.enum_def[abs_def]
by (auto simp add: 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 \<open>a = enum i\<close>
using inj_on_image_set_diff[OF inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
inj_on_image_set_diff[OF b.inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
by (simp add: comp_def)
have "a \<noteq> b.enum i"
using \<open>a = enum i\<close> enum_eq_benum i by auto
{ fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
obtain b' u where "kuhn_simplex p n b' u t"
using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b' u t .
have "enum i' \<in> s - {a}" "enum (i + 1) \<in> s - {a}"
using \<open>a = enum i\<close> i enum_in by (auto simp: enum_inj i'_def)
then obtain l k where
l: "t.enum l = enum i'" "l \<le> n" "t.enum l \<noteq> c" and
k: "t.enum k = enum (i + 1)" "k \<le> n" "t.enum k \<noteq> 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 \<open>l \<le> n\<close> \<open>k \<le> n\<close> 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 \<open>Suc l = k\<close> i'_def)
then have False
using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
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 \<open>l < k\<close> have "Suc l < k"
by arith
have c_eq: "c = t.enum (Suc l)"
proof (rule ccontr)
assume "c \<noteq> t.enum (Suc l)"
then have "t.enum (Suc l) \<in> s - {a}"
using \<open>l < k\<close> \<open>k \<le> n\<close> by (simp add: t.s_eq eq_sma)
then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
unfolding s_eq \<open>a = enum i\<close> by auto
with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
by (auto simp add: i'_def enum_mono enum_inj l k)
with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
by (simp add: t.enum_mono)
qed
{ have "t.enum (Suc (Suc l)) \<in> s - {a}"
unfolding eq_sma c_eq t.s_eq using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_inj)
then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \<le> n" "j \<noteq> i"
by (auto simp: s_eq \<open>a = enum i\<close>)
moreover have "enum i' < t.enum (Suc (Suc l))"
unfolding l(1)[symmetric] using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_strict_mono)
ultimately have "i' < j"
using i by (simp add: enum_strict_mono i'_def)
with \<open>j \<noteq> i\<close> \<open>j \<le> n\<close> have "t.enum k \<le> t.enum (Suc (Suc l))"
unfolding i'_def by (simp add: enum_mono k eq)
then have "k \<le> Suc (Suc l)"
using \<open>k \<le> n\<close> \<open>Suc l < k\<close> by (simp add: t.enum_mono) }
with \<open>Suc l < k\<close> 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 "\<dots> = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
(u l = upd (Suc i') \<and> u (Suc l) = upd i')"
using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)
then have "t = s \<or> 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 \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close> by (simp add: enum_Suc t.enum_Suc l)
also have "\<dots> = a"
using \<open>a = enum i\<close> i by (simp add: i'_def)
finally show ?thesis
using eq_sma \<open>a \<in> s\<close> \<open>c \<in> t\<close> 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 add: 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 \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close> swap_apply1)
(simp add: Suc_i')
also have "\<dots> = b.enum i"
using i by (simp add: i'_def)
finally have "c = b.enum i" .
then have "t - {c} = B - {c}" "c \<in> B"
unfolding eq_sma[symmetric] eq B_def using i by auto
with \<open>c \<in> t\<close> have "t = B"
by auto
then show ?thesis
by (simp add: B_def)
qed }
with ks_f' eq \<open>a \<noteq> b.enum i\<close> \<open>n \<noteq> 0\<close> \<open>i \<le> n\<close> show ?thesis
apply (intro ex1I[of _ "b.enum ` {.. n}"])
apply auto []
apply metis
done
qed
then show ?thesis
using s \<open>a \<in> s\<close> by (simp add: card_2_exists Ex1_def) metis
qed
text \<open>Hence another step towards concreteness.\<close>
lemma kuhn_simplex_lemma:
assumes "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> rl ` s \<subseteq> {.. Suc n}"
and "odd (card {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
rl ` f = {..n} \<and> ((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p))})"
shows "odd (card {s. ksimplex p (Suc n) s \<and> rl ` s = {..Suc n}})"
proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
where bnd="\<lambda>f. (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p)"],
safe del: notI)
have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
by auto
show "odd (card {f. (\<exists>s\<in>{s. ksimplex p (Suc n) s}. \<exists>a\<in>s. f = s - {a}) \<and>
rl ` f = {..n} \<and> ((\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>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 \<in> s" then show "rl a \<le> Suc n"
using assms(1) s by (auto simp: subset_eq)
let ?S = "{t. ksimplex p (Suc n) t \<and> (\<exists>b\<in>t. s - {a} = t - {b})}"
{ fix j assume j: "j \<le> n" "\<forall>x\<in>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 \<le> n" "\<forall>x\<in>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 \<noteq> 2" "\<not> (\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = p)"
with s a show "\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = 0"
using ksimplex_replace_2[of p "n + 1" s a]
by (subst (asm) eq_commute) auto }
qed
subsection \<open>Reduced labelling\<close>
definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"
lemma reduced_labelling:
shows "reduced n x \<le> n"
and "\<forall>i<reduced n x. x i = 0"
and "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
proof -
show "reduced n x \<le> n"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
show "\<forall>i<reduced n x. x i = 0"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
show "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
qed
lemma reduced_labelling_unique:
"r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> 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 \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> 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 \<Longrightarrow> x j \<noteq> 0 \<Longrightarrow> reduced n x \<le> j"
using reduced_labelling[of n x] by (elim allE[where x=j]) auto
lemma reduced_labelling_Suc: "reduced (Suc n) x \<noteq> Suc n \<Longrightarrow> 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 "\<forall>x\<in>f. \<forall>j\<le>n. x j = 0 \<longrightarrow> lab x j = 0"
and "\<forall>x\<in>f. \<forall>j\<le>n. x j = p \<longrightarrow> lab x j = 1"
and eq: "(reduced (Suc n) \<circ> lab) ` f = {..n}"
shows "((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p)) \<longleftrightarrow> (\<forall>x\<in>f. x n = p)"
proof (safe del: disjCI)
fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = 0"
{ fix x assume "x \<in> f" with assms j have "reduced (Suc n) (lab x) \<noteq> j"
by (intro reduced_labelling_zero) auto }
moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
using j eq by auto
ultimately show "x n = p"
by force
next
fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = p" and x: "x \<in> f"
have "j = n"
proof (rule ccontr)
assume "\<not> ?thesis"
{ fix x assume "x \<in> f"
with assms j have "reduced (Suc n) (lab x) \<le> j"
by (intro reduced_labelling_nonzero) auto
then have "reduced (Suc n) (lab x) \<noteq> n"
using \<open>j \<noteq> n\<close> \<open>j \<le> n\<close> by simp }
moreover
have "n \<in> (reduced (Suc n) \<circ> lab) ` f"
using eq by auto
ultimately show False
by force
qed
moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
using j eq by auto
ultimately show "x n = p"
using j x by auto
qed auto
text \<open>Hence we get just about the nice induction.\<close>
lemma kuhn_induction:
assumes "0 < p"
and lab_0: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
and lab_1: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
and odd: "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
shows "odd (card {s. ksimplex p (Suc n) s \<and> (reduced (Suc n)\<circ>lab) ` s = {..Suc n}})"
proof -
let ?rl = "reduced (Suc n) \<circ> lab" and ?ext = "\<lambda>f v. \<exists>j\<le>n. \<forall>x\<in>f. x j = v"
let ?ext = "\<lambda>s. (\<exists>j\<le>n. \<forall>x\<in>s. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>s. x j = p)"
have "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> ?rl ` s \<subseteq> {..Suc n}"
by (simp add: reduced_labelling subset_eq)
moreover
have "{s. ksimplex p n s \<and> (reduced n \<circ> lab) ` s = {..n}} =
{f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
proof (intro set_eqI, safe del: disjCI equalityI disjE)
fix s assume s: "ksimplex p n s" and rl: "(reduced n \<circ> 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: "\<forall>x\<in>s. x n = p"
by (auto simp: out_eq_p)
moreover
{ fix x assume "x \<in> s"
with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
have "?rl x \<le> 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 \<in> t" "s = t - {a}"
using s unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] by auto
ultimately
show "\<exists>t a. ksimplex p (Suc n) t \<and> a \<in> t \<and> s = t - {a} \<and> ?rl ` s = {..n} \<and> ?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 \<in> 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: "\<forall>x\<in>s. x (Suc n) = p"
by (auto simp: out_eq_p)
{ fix x assume "x \<in> s - {a}"
then have "?rl x \<in> ?rl ` (s - {a})"
by auto
then have "?rl x \<le> n"
unfolding rl by auto
then have "?rl x = reduced n (lab x)"
by (auto intro!: reduced_labelling_Suc) }
then show rl': "(reduced n\<circ>lab) ` (s - {a}) = {..n}"
unfolding rl[symmetric] by (intro image_cong) auto
from \<open>?ext (s - {a})\<close>
have all_eq_p: "\<forall>x\<in>s - {a}. x n = p"
proof (elim disjE exE conjE)
fix j assume "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
with lab_0[rule_format, of j] all_eq_p s_le_p
have "\<And>x. x \<in> s - {a} \<Longrightarrow> reduced (Suc n) (lab x) \<noteq> j"
by (intro reduced_labelling_zero) auto
moreover have "j \<in> ?rl ` (s - {a})"
using \<open>j \<le> n\<close> unfolding rl by auto
ultimately show ?thesis
by force
next
fix j assume "j \<le> n" and eq_p: "\<forall>x\<in>s - {a}. x j = p"
show ?thesis
proof cases
assume "j = n" with eq_p show ?thesis by simp
next
assume "j \<noteq> n"
{ fix x assume x: "x \<in> s - {a}"
have "reduced n (lab x) \<le> j"
proof (rule reduced_labelling_nonzero)
show "lab x j \<noteq> 0"
using lab_1[rule_format, of j x] x s_le_p[of x] eq_p \<open>j \<le> n\<close> by auto
show "j < n"
using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp
qed
then have "reduced n (lab x) \<noteq> n"
using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp }
moreover have "n \<in> (reduced n\<circ>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 \<open>0 < p\<close> all_eq_p] using s a by auto
qed
ultimately show ?thesis
using assms by (intro kuhn_simplex_lemma) auto
qed
text \<open>And so we get the final combinatorial result.\<close>
lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
proof
assume "ksimplex p 0 s" then show "s = {(\<lambda>x. p)}"
by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
next
assume s: "s = {(\<lambda>x. p)}"
show "ksimplex p 0 s"
proof (intro ksimplex, unfold_locales)
show "(\<lambda>_. p) \<in> {..<0::nat} \<rightarrow> {..<p}" by auto
show "bij_betw id {..<0} {..<0}"
by simp
qed (auto simp: s)
qed
lemma kuhn_combinatorial:
assumes "0 < p"
and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = 0 \<longrightarrow> lab x j = 0"
and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = p \<longrightarrow> lab x j = 1"
shows "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>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 "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. label x i = (0::nat) \<or> label x i = 1)"
and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow> label x i = 0)"
and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow> label x i = 1)"
obtains q where "\<forall>i<n. q i < p"
and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
proof -
let ?rl = "reduced n \<circ> label"
let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
have "odd (card ?A)"
using assms by (intro kuhn_combinatorial[of p n label]) auto
then have "?A \<noteq> {}"
by fastforce
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 \<in> {.. n}" "Suc i \<in> {.. n}"
by auto
then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
unfolding rl[symmetric] by blast
have "label u i \<noteq> label v i"
using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
by auto
moreover
have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1" if "j < n" for j
using that base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>]
by auto
ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
(\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
by blast
qed
qed
subsection \<open>The main result for the unit cube\<close>
lemma kuhn_labelling_lemma':
assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
(\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
(\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
(\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
(\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
proof -
have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
by auto
have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
by auto
show ?thesis
unfolding and_forall_thm
apply (subst choice_iff[symmetric])+
apply rule
apply rule
proof -
fix x x'
let ?R = "\<lambda>y::nat.
(P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
(P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
(P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
(P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
have "0 \<le> f x x' \<and> f x x' \<le> 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 \<or> ?R 1"
by auto
then show "\<exists>y\<le>1. ?R y"
by auto
qed
qed
definition unit_cube :: "'a::euclidean_space set"
where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
unfolding unit_cube_def by simp
lemma bounded_unit_cube: "bounded unit_cube"
unfolding bounded_def
proof (intro exI ballI)
fix y :: 'a assume y: "y \<in> unit_cube"
have "dist 0 y = norm y" by (rule dist_0_norm)
also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_setsum)
also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
by (rule setsum_mono, simp add: y [unfolded mem_unit_cube])
finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
qed
lemma closed_unit_cube: "closed unit_cube"
unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
unfolding compact_eq_seq_compact_metric
using bounded_unit_cube closed_unit_cube
by (rule bounded_closed_imp_seq_compact)
lemma brouwer_cube:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes "continuous_on unit_cube f"
and "f ` unit_cube \<subseteq> unit_cube"
shows "\<exists>x\<in>unit_cube. f x = x"
proof (rule ccontr)
define n where "n = DIM('a)"
have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
assume "\<not> ?thesis"
then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
by auto
obtain d where
d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
apply (rule continuous_intros assms)+
apply blast
done
have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
"\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
using assms(2)[unfolded image_subset_iff Ball_def]
unfolding mem_unit_cube
by auto
obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
"\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
"\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
"\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
"\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
"\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
using kuhn_labelling_lemma[OF *] by blast
note label = this [rule_format]
have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
proof safe
fix x y :: 'a
assume x: "x \<in> unit_cube"
assume y: "y \<in> unit_cube"
fix i
assume i: "label x i \<noteq> label y i" "i \<in> Basis"
have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
\<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
unfolding inner_simps
apply (rule *)
apply (cases "label x i = 0")
apply (rule disjI1)
apply rule
prefer 3
apply (rule disjI2)
apply rule
proof -
assume lx: "label x i = 0"
then have ly: "label y i = 1"
using i label(1)[of i y]
by auto
show "x \<bullet> i \<le> f x \<bullet> i"
apply (rule label(4)[rule_format])
using x y lx i(2)
apply auto
done
show "f y \<bullet> i \<le> y \<bullet> i"
apply (rule label(5)[rule_format])
using x y ly i(2)
apply auto
done
next
assume "label x i \<noteq> 0"
then have l: "label x i = 1" "label y i = 0"
using i label(1)[of i x] label(1)[of i y]
by auto
show "f x \<bullet> i \<le> x \<bullet> i"
apply (rule label(5)[rule_format])
using x y l i(2)
apply auto
done
show "y \<bullet> i \<le> f y \<bullet> i"
apply (rule label(4)[rule_format])
using x y l i(2)
apply auto
done
qed
also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
apply (rule add_mono)
apply (rule Basis_le_norm[OF i(2)])+
done
finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
unfolding inner_simps .
qed
have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
\<bar>(f(z) - z)\<bullet>i\<bar> < 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 unit_cube f"
by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
obtain e where e:
"e > 0"
"\<And>x x'. x \<in> unit_cube \<Longrightarrow>
x' \<in> unit_cube \<Longrightarrow>
norm (x' - x) < e \<Longrightarrow>
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
apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
apply safe
proof -
show "0 < min (e / 2) (d / real n / 8)"
using d' e by auto
fix x y z i
assume as:
"x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
"norm (x - z) < min (e / 2) (d / real n / 8)"
"norm (y - z) < min (e / 2) (d / real n / 8)"
"label x i \<noteq> label y i"
assume i: "i \<in> Basis"
have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
\<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
(8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
by auto
show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
unfolding inner_simps
proof (rule *)
show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
apply (rule lem1[rule_format])
using as i
apply auto
done
show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
unfolding inner_diff_left[symmetric]
by (rule Basis_le_norm[OF i])+
have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
using dist_triangle[of y x z, unfolded dist_norm]
unfolding norm_minus_commute
by auto
also have "\<dots> < e / 2 + e / 2"
apply (rule add_strict_mono)
using as(4,5)
apply auto
done
finally show "norm (f y - f x) < d / real n / 8"
apply -
apply (rule e(2))
using as
apply auto
done
have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
apply (rule add_strict_mono)
using as
apply auto
done
then show "norm (y - x) < 2 * (d / real n / 8)"
using tria
by auto
show "norm (f x - f z) < d / real n / 8"
apply (rule e(2))
using as e(1)
apply auto
done
qed (insert as, auto)
qed
qed
then
obtain e where e:
"e > 0"
"\<And>x y z i. x \<in> unit_cube \<Longrightarrow>
y \<in> unit_cube \<Longrightarrow>
z \<in> unit_cube \<Longrightarrow>
i \<in> Basis \<Longrightarrow>
norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
by blast
obtain p :: nat where p: "1 + real n / e \<le> 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 \<Rightarrow> '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: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {..< n}"
unfolding bij_betw_def by (auto simp: set_eq_iff)
have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
unfolding b'_def
using b
by (auto simp: f_inv_into_f bij_betw_def)
have b'b[simp]:"\<And>i. i < n \<Longrightarrow> b' (b i) = i"
unfolding b'_def
using b
by (auto simp: inv_into_f_eq bij_betw_def)
have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
by auto
have b'': "\<And>j. j < n \<Longrightarrow> b j \<in> Basis"
using b unfolding bij_betw_def by auto
have q1: "0 < p" "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow>
(\<forall>i<n. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
unfolding *
using \<open>p > 0\<close> \<open>n > 0\<close>
using label(1)[OF b'']
by auto
{ fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
using b'_Basis
by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
note cube = this
have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp add: b'')
have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
obtain q where q:
"\<forall>i<n. q i < p"
"\<forall>i<n.
\<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
(\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
(label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
by (rule kuhn_lemma[OF q1 q2 q3])
define z :: 'a where "z = (\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)"
have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
proof (rule ccontr)
have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
using q(1) b'
by (auto intro: less_imp_le simp: bij_betw_def)
then have "z \<in> unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
then have d_fz_z: "d \<le> norm (f z - z)"
by (rule d)
assume "\<not> ?thesis"
then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
using \<open>n > 0\<close>
by (auto simp add: not_le inner_diff)
have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
unfolding inner_diff_left[symmetric]
by (rule norm_le_l1)
also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
apply (rule setsum_strict_mono)
using as
apply auto
done
also have "\<dots> = 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 \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
have *: "b' i < n"
using i and b'[unfolded bij_betw_def]
by auto
obtain r s where rs:
"\<And>j. j < n \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
"\<And>j. j < n \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
"(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
(label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
using q(2)[rule_format,OF *] by blast
have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow> b' i < n"
using b' unfolding bij_betw_def by auto
define r' ::'a where "r' = (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)"
have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> 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 add: Suc_le_eq)
done
then have "r' \<in> unit_cube"
unfolding r'_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
apply (rule order_trans)
apply (rule rs(2)[OF b'_im, THEN conjunct2])
using q(1)[rule_format,OF b'_im]
apply (auto simp add: Suc_le_eq)
done
then have "s' \<in> unit_cube"
unfolding s'_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
have "z \<in> unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
have *: "\<And>x. 1 + real x = real (Suc x)"
by auto
{
have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(1)[OF b'_im]
apply (auto simp add:* field_simps simp del: of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
by (auto simp add: field_simps n_def)
finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
}
moreover
{
have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(2)[OF b'_im]
apply (auto simp add:* field_simps simp del: of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
by (auto simp add: field_simps n_def)
finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
}
ultimately
have "norm (r' - z) < e" and "norm (s' - z) < e"
unfolding r'_def s'_def z_def
using \<open>p > 0\<close>
apply (rule_tac[!] le_less_trans[OF norm_le_l1])
apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
done
then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
using rs(3) i
unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
by (intro e(2)[OF \<open>r'\<in>unit_cube\<close> \<open>s'\<in>unit_cube\<close> \<open>z\<in>unit_cube\<close>]) auto
then show False
using i by auto
qed
subsection \<open>Retractions\<close>
definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
definition retract_of (infixl "retract'_of" 50)
where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow> r (r x) = r x"
unfolding retraction_def by auto
subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
lemma invertible_fixpoint_property:
fixes s :: "'a::euclidean_space set"
and t :: "'b::euclidean_space set"
assumes "continuous_on t i"
and "i ` t \<subseteq> s"
and "continuous_on s r"
and "r ` s \<subseteq> t"
and "\<forall>y\<in>t. r (i y) = y"
and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
and "continuous_on t g"
and "g ` t \<subseteq> t"
obtains y where "y \<in> t" and "g y = y"
proof -
have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
apply (rule assms(6)[rule_format])
apply rule
apply (rule continuous_on_compose assms)+
apply ((rule continuous_on_subset)?, rule assms)+
using assms(2,4,8)
apply auto
apply blast
done
then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
then have *: "g (r x) \<in> t"
using assms(4,8) by auto
have "r ((i \<circ> g \<circ> r) x) = r x"
using x by auto
then show ?thesis
apply (rule_tac that[of "r x"])
using x
unfolding o_def
unfolding assms(5)[rule_format,OF *]
using assms(4)
apply auto
done
qed
lemma homeomorphic_fixpoint_property:
fixes s :: "'a::euclidean_space set"
and t :: "'b::euclidean_space set"
assumes "s homeomorphic t"
shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
(\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
proof -
obtain r i where
"\<forall>x\<in>s. i (r x) = x"
"r ` s = t"
"continuous_on s r"
"\<forall>y\<in>t. r (i y) = y"
"i ` t = s"
"continuous_on t i"
using assms
unfolding homeomorphic_def homeomorphism_def
by blast
then show ?thesis
apply -
apply rule
apply (rule_tac[!] allI impI)+
apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
prefer 10
apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
apply auto
done
qed
lemma retract_fixpoint_property:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
and s :: "'a set"
assumes "t retract_of s"
and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
and "continuous_on t g"
and "g ` t \<subseteq> t"
obtains y where "y \<in> t" and "g y = y"
proof -
obtain h where "retraction s t h"
using assms(1) unfolding retract_of_def ..
then show ?thesis
unfolding retraction_def
apply -
apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
prefer 7
apply (rule_tac y = y in that)
using assms
apply auto
done
qed
subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
lemma convex_unit_cube: "convex unit_cube"
apply (rule is_interval_convex)
apply (clarsimp simp add: is_interval_def mem_unit_cube)
apply (drule (1) bspec)+
apply auto
done
lemma brouwer_weak:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes "compact s"
and "convex s"
and "interior s \<noteq> {}"
and "continuous_on s f"
and "f ` s \<subseteq> s"
obtains x where "x \<in> s" and "f x = x"
proof -
let ?U = "unit_cube :: 'a set"
have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
proof (rule interiorI)
let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> 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 "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
by simp
show "?I \<subseteq> unit_cube"
unfolding unit_cube_def by force
qed
then have *: "interior ?U \<noteq> {}" by fast
have *: "?U homeomorphic s"
using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
(\<exists>x\<in>?U. f x = x)"
using brouwer_cube by auto
then show ?thesis
unfolding homeomorphic_fixpoint_property[OF *]
using assms
by (auto simp: intro: that)
qed
text \<open>And in particular for a closed ball.\<close>
lemma brouwer_ball:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes "e > 0"
and "continuous_on (cball a e) f"
and "f ` cball a e \<subseteq> cball a e"
obtains x where "x \<in> 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 \<open>Still more general form; could derive this directly without using the
rather involved \<open>HOMEOMORPHIC_CONVEX_COMPACT\<close> theorem, just using
a scaling and translation to put the set inside the unit cube.\<close>
lemma brouwer:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes "compact s"
and "convex s"
and "s \<noteq> {}"
and "continuous_on s f"
and "f ` s \<subseteq> s"
obtains x where "x \<in> s" and "f x = x"
proof -
have "\<exists>e>0. s \<subseteq> cball 0 e"
using compact_imp_bounded[OF assms(1)]
unfolding bounded_pos
apply (erule_tac exE)
apply (rule_tac x=b in exI)
apply (auto simp add: dist_norm)
done
then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
by blast
have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
apply (rule continuous_on_compose )
apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
apply (rule continuous_on_subset[OF assms(4)])
apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
using assms(5)[unfolded subset_eq]
using e(2)[unfolded subset_eq mem_cball]
apply (auto simp add: dist_norm)
done
then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
have *: "closest_point s x = x"
apply (rule closest_point_self)
apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
apply (rule_tac x="closest_point s x" in bexI)
using x
unfolding o_def
using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
apply auto
done
show thesis
apply (rule_tac x="closest_point s x" in that)
unfolding x(2)[unfolded o_def]
apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
using *
apply auto
done
qed
text \<open>So we get the no-retraction theorem.\<close>
lemma no_retraction_cball:
fixes a :: "'a::euclidean_space"
assumes "e > 0"
shows "\<not> (frontier (cball a e) retract_of (cball a e))"
proof
assume *: "frontier (cball a e) retract_of (cball a e)"
have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
using scaleR_left_distrib[of 1 1 a] by auto
obtain x where x:
"x \<in> {x. norm (a - x) = e}"
"2 *\<^sub>R a - x = x"
apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
apply (blast intro: brouwer_ball[OF assms])
apply (intro continuous_intros)
unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
apply (auto simp add: ** norm_minus_commute)
done
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
by (auto simp add: algebra_simps)
then have "a = x"
unfolding scaleR_left_distrib[symmetric]
by auto
then show False
using x assms by auto
qed
subsection\<open>Retractions\<close>
lemma retraction:
"retraction s t r \<longleftrightarrow>
t \<subseteq> s \<and> continuous_on s r \<and> r ` s = t \<and> (\<forall>x \<in> t. r x = x)"
by (force simp: retraction_def)
lemma retract_of_imp_extensible:
assumes "s retract_of t" and "continuous_on s f" and "f ` s \<subseteq> u"
obtains g where "continuous_on t g" "g ` t \<subseteq> u" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
using assms
apply (clarsimp simp add: retract_of_def retraction)
apply (rule_tac g = "f o r" in that)
apply (auto simp: continuous_on_compose2)
done
lemma idempotent_imp_retraction:
assumes "continuous_on s f" and "f ` s \<subseteq> s" and "\<And>x. x \<in> s \<Longrightarrow> f(f x) = f x"
shows "retraction s (f ` s) f"
by (simp add: assms retraction)
lemma retraction_subset:
assumes "retraction s t r" and "t \<subseteq> s'" and "s' \<subseteq> s"
shows "retraction s' t r"
apply (simp add: retraction_def)
by (metis assms continuous_on_subset image_mono retraction)
lemma retract_of_subset:
assumes "t retract_of s" and "t \<subseteq> s'" and "s' \<subseteq> s"
shows "t retract_of s'"
by (meson assms retract_of_def retraction_subset)
lemma retraction_refl [simp]: "retraction s s (\<lambda>x. x)"
by (simp add: continuous_on_id retraction)
lemma retract_of_refl [iff]: "s retract_of s"
using continuous_on_id retract_of_def retraction_def by fastforce
lemma retract_of_imp_subset:
"s retract_of t \<Longrightarrow> s \<subseteq> t"
by (simp add: retract_of_def retraction_def)
lemma retract_of_empty [simp]:
"({} retract_of s) \<longleftrightarrow> s = {}" "(s retract_of {}) \<longleftrightarrow> s = {}"
by (auto simp: retract_of_def retraction_def)
lemma retract_of_singleton [iff]: "({x} retract_of s) \<longleftrightarrow> x \<in> s"
using continuous_on_const
by (auto simp: retract_of_def retraction_def)
lemma retraction_comp:
"\<lbrakk>retraction s t f; retraction t u g\<rbrakk>
\<Longrightarrow> retraction s u (g o f)"
apply (auto simp: retraction_def intro: continuous_on_compose2)
by blast
lemma retract_of_trans [trans]:
assumes "s retract_of t" and "t retract_of u"
shows "s retract_of u"
using assms by (auto simp: retract_of_def intro: retraction_comp)
lemma closedin_retract:
fixes s :: "'a :: real_normed_vector set"
assumes "s retract_of t"
shows "closedin (subtopology euclidean t) s"
proof -
obtain r where "s \<subseteq> t" "continuous_on t r" "r ` t \<subseteq> s" "\<And>x. x \<in> s \<Longrightarrow> r x = x"
using assms by (auto simp: retract_of_def retraction_def)
then have s: "s = {x \<in> t. (norm(r x - x)) = 0}" by auto
show ?thesis
apply (subst s)
apply (rule continuous_closedin_preimage_constant)
by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
qed
lemma closedin_self [simp]:
fixes S :: "'a :: real_normed_vector set"
shows "closedin (subtopology euclidean S) S"
by (simp add: closedin_retract)
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 o h" in exI)
apply (intro conjI continuous_intros continuous_on_compose)
apply (erule continuous_on_subset | force)+
done
lemma retract_of_compact:
"\<lbrakk>compact t; s retract_of t\<rbrakk> \<Longrightarrow> compact s"
by (metis compact_continuous_image retract_of_def retraction)
lemma retract_of_closed:
fixes s :: "'a :: real_normed_vector set"
shows "\<lbrakk>closed t; s retract_of t\<rbrakk> \<Longrightarrow> closed s"
by (metis closedin_retract closedin_closed_eq)
lemma retract_of_connected:
"\<lbrakk>connected t; s retract_of t\<rbrakk> \<Longrightarrow> connected s"
by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
lemma retract_of_path_connected:
"\<lbrakk>path_connected t; s retract_of t\<rbrakk> \<Longrightarrow> path_connected s"
by (metis path_connected_continuous_image retract_of_def retraction)
lemma retract_of_simply_connected:
"\<lbrakk>simply_connected t; s retract_of t\<rbrakk> \<Longrightarrow> simply_connected s"
apply (simp add: retract_of_def retraction_def, clarify)
apply (rule simply_connected_retraction_gen)
apply (force simp: continuous_on_id elim!: continuous_on_subset)+
done
lemma retract_of_homotopically_trivial:
assumes ts: "t retract_of s"
and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s;
continuous_on u g; g ` u \<subseteq> s\<rbrakk>
\<Longrightarrow> homotopic_with (\<lambda>x. True) u s f g"
and "continuous_on u f" "f ` u \<subseteq> t"
and "continuous_on u g" "g ` u \<subseteq> t"
shows "homotopic_with (\<lambda>x. True) u t f g"
proof -
obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>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: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) u s f (\<lambda>x. c)"
and "continuous_on u f" "f ` u \<subseteq> t"
obtains c where "homotopic_with (\<lambda>x. True) u t f (\<lambda>x. c)"
proof -
obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>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_imp_quotient_map:
"retraction s t r
\<Longrightarrow> u \<subseteq> t
\<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> r x \<in> u} \<longleftrightarrow>
openin (subtopology euclidean t) u)"
apply (clarsimp simp add: retraction)
apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
apply (auto simp: elim: continuous_on_subset)
done
lemma retract_of_locally_compact:
fixes s :: "'a :: {heine_borel,real_normed_vector} set"
shows "\<lbrakk> locally compact s; t retract_of s\<rbrakk> \<Longrightarrow> locally compact t"
by (metis locally_compact_closedin closedin_retract)
lemma retract_of_Times:
"\<lbrakk>s retract_of s'; t retract_of t'\<rbrakk> \<Longrightarrow> (s \<times> t) retract_of (s' \<times> t')"
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
apply (rename_tac f g)
apply (rule_tac x="\<lambda>z. ((f o fst) z, (g o snd) z)" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
done
lemma homotopic_into_retract:
"\<lbrakk>f ` s \<subseteq> t; g ` s \<subseteq> t; t retract_of u;
homotopic_with (\<lambda>x. True) s u f g\<rbrakk>
\<Longrightarrow> homotopic_with (\<lambda>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 o 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: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image)
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: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
subsection\<open>Punctured affine hulls, etc.\<close>
lemma continuous_on_compact_surface_projection_aux:
fixes S :: "'a::t2_space set"
assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
and contp: "continuous_on T p"
and "\<And>x. x \<in> S \<Longrightarrow> q x = x"
and [simp]: "\<And>x. x \<in> T \<Longrightarrow> q(p x) = q x"
and "\<And>x. x \<in> T \<Longrightarrow> 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 \<open>S \<subseteq> T\<close>])
have "continuous_on T (q \<circ> p)"
apply (rule continuous_on_compose [OF contp])
apply (simp add: *)
apply (rule continuous_on_inv [OF contp' \<open>compact S\<close>])
using assms by auto
then show ?thesis
apply (rule continuous_on_eq [of _ "q o p"])
apply (simp add: o_def)
done
qed
lemma continuous_on_compact_surface_projection:
fixes S :: "'a::real_normed_vector set"
assumes "compact S"
and S: "S \<subseteq> V - {0}" and "cone V"
and iff: "\<And>x k. x \<in> V - {0} \<Longrightarrow> 0 < k \<and> (k *\<^sub>R x) \<in> S \<longleftrightarrow> d x = k"
shows "continuous_on (V - {0}) (\<lambda>x. d x *\<^sub>R x)"
proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
show "(\<lambda>x. d x *\<^sub>R x) ` (V - {0}) \<subseteq> S"
using iff by auto
show "continuous_on (V - {0}) (\<lambda>x. inverse(norm x) *\<^sub>R x)"
by (intro continuous_intros) force
show "\<And>x. x \<in> S \<Longrightarrow> d x *\<^sub>R x = x"
by (metis S zero_less_one local.iff scaleR_one subset_eq)
show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \<in> V - {0}" for x
using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \<open>cone V\<close>
by (simp add: field_simps cone_def zero_less_mult_iff)
show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \<in> V - {0}" for x
proof -
have "0 < d x"
using local.iff that by blast
then show ?thesis
by simp
qed
qed
proposition rel_frontier_deformation_retract_of_punctured_convex:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "convex T" "bounded S"
and arelS: "a \<in> rel_interior S"
and relS: "rel_frontier S \<subseteq> T"
and affS: "T \<subseteq> affine hull S"
obtains r where "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id r"
"retraction (T - {a}) (rel_frontier S) r"
proof -
have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
(\<forall>e. 0 \<le> e \<and> e < d \<longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S)"
if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> arelS])
apply (rule that)+
by metis
then obtain dd
where dd1: "\<And>l. \<lbrakk>(a + l) \<in> affine hull S; l \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < dd l \<and> (a + dd l *\<^sub>R l) \<in> rel_frontier S"
and dd2: "\<And>l e. \<lbrakk>(a + l) \<in> affine hull S; e < dd l; 0 \<le> e; l \<noteq> 0\<rbrakk>
\<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
by metis+
have aaffS: "a \<in> affine hull S"
by (meson arelS subsetD hull_inc rel_interior_subset)
have "((\<lambda>z. z - a) ` (affine hull S - {a})) = ((\<lambda>z. z - a) ` (affine hull S)) - {0}"
by (auto simp: )
moreover have "continuous_on (((\<lambda>z. z - a) ` (affine hull S)) - {0}) (\<lambda>x. dd x *\<^sub>R x)"
proof (rule continuous_on_compact_surface_projection)
show "compact (rel_frontier ((\<lambda>z. z - a) ` S))"
by (simp add: \<open>bounded S\<close> bounded_translation_minus compact_rel_frontier_bounded)
have releq: "rel_frontier ((\<lambda>z. z - a) ` S) = (\<lambda>z. z - a) ` rel_frontier S"
using rel_frontier_translation [of "-a"] add.commute by simp
also have "... \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
using rel_frontier_affine_hull arelS rel_frontier_def by fastforce
finally show "rel_frontier ((\<lambda>z. z - a) ` S) \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}" .
show "cone ((\<lambda>z. z - a) ` (affine hull S))"
apply (rule subspace_imp_cone)
using aaffS
apply (simp add: subspace_affine image_comp o_def affine_translation_aux [of a])
done
show "(0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)) \<longleftrightarrow> (dd x = k)"
if x: "x \<in> (\<lambda>z. z - a) ` (affine hull S) - {0}" for k x
proof
show "dd x = k \<Longrightarrow> 0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
using dd1 [of x] that image_iff by (fastforce simp add: releq)
next
assume k: "0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
have False if "dd x < k"
proof -
have "k \<noteq> 0" "a + k *\<^sub>R x \<in> closure S"
using k closure_translation [of "-a"]
by (auto simp: rel_frontier_def)
then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
using x by (auto simp: )
then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
using dd1 by auto
moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
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) \<open>k \<noteq> 0\<close> divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse)
done
ultimately show ?thesis
using segsub by (auto simp add: 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 ((\<lambda>z. z - a) ` (affine hull S - {a})) (\<lambda>x. dd x *\<^sub>R x)"
by auto
have "continuous_on (affine hull S - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
by (intro * continuous_intros continuous_on_compose)
with affS have contdd: "continuous_on (T - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
by (blast intro: continuous_on_subset elim: )
show ?thesis
proof
show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>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}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
using contdd by (simp add: o_def)
show "closed_segment (id x) (a + dd (x - a) *\<^sub>R (x - a)) \<subseteq> T - {a}"
if "x \<in> T - {a}" for x
proof (clarsimp simp: in_segment, intro conjI)
fix u::real assume u: "0 \<le> u" "u \<le> 1"
show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
apply (rule convexD [OF \<open>convex T\<close>])
using that u apply (auto simp add: )
apply (metis add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 relS subsetD)
done
have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
(1 - u + u * d) *\<^sub>R (x - a) = 0" for d
by (auto simp: algebra_simps)
have "x \<in> T" "x \<noteq> a" using that by auto
then have axa: "a + (x - a) \<in> affine hull S"
by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp)
then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
using \<open>x \<noteq> a\<close> dd1 by fastforce
with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> 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) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
proof (simp add: retraction_def, intro conjI ballI)
show "rel_frontier S \<subseteq> T - {a}"
using arelS relS rel_frontier_def by fastforce
show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
using contdd by (simp add: o_def)
show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) ` (T - {a}) \<subseteq> 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) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
proof -
have "x \<noteq> a"
using that arelS by (auto simp add: rel_frontier_def)
have False if "dd (x - a) < 1"
proof -
have "x \<in> closure S"
using x by (auto simp: rel_frontier_def)
then have segsub: "open_segment a x \<subseteq> rel_interior S"
by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
have xaffS: "x \<in> affine hull S"
using affS relS x by auto
then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
using dd1 by (auto simp add: \<open>x \<noteq> a\<close>)
moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
using \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
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 add: rel_frontier_def)
qed
moreover have False if "1 < dd (x - a)"
using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
by (auto simp: rel_frontier_def)
ultimately have "dd (x - a) = 1" --\<open>similar to another proof above\<close>
by fastforce
with that show ?thesis
by (simp add: rel_frontier_def)
qed
qed
qed
qed
corollary rel_frontier_retract_of_punctured_affine_hull:
fixes S :: "'a::euclidean_space set"
assumes "bounded S" "convex S" "a \<in> rel_interior S"
shows "rel_frontier S retract_of (affine hull S - {a})"
apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
apply (auto simp add: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
done
corollary rel_boundary_retract_of_punctured_affine_hull:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S" "a \<in> rel_interior S"
shows "(S - rel_interior S) retract_of (affine hull S - {a})"
by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
rel_frontier_retract_of_punctured_affine_hull)
subsection\<open>Borsuk-style characterization of separation\<close>
lemma continuous_on_Borsuk_map:
"a \<notin> s \<Longrightarrow> continuous_on s (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
by (rule continuous_intros | force)+
lemma Borsuk_map_into_sphere:
"(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \<subseteq> sphere 0 1 \<longleftrightarrow> (a \<notin> s)"
by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero)
lemma Borsuk_maps_homotopic_in_path_component:
assumes "path_component (- s) a b"
shows "homotopic_with (\<lambda>x. True) s (sphere 0 1)
(\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
(\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
proof -
obtain g where "path g" "path_image g \<subseteq> -s" "pathstart g = a" "pathfinish g = b"
using assms by (auto simp: path_component_def)
then show ?thesis
apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g o fst)z)) *\<^sub>R (snd z - (g o fst)z)" in exI)
apply (intro conjI continuous_intros)
apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
done
qed
lemma non_extensible_Borsuk_map:
fixes a :: "'a :: euclidean_space"
assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
shows "~ (\<exists>g. continuous_on (s \<union> c) g \<and>
g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
(\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
proof -
have "closed s" using assms by (simp add: compact_imp_closed)
have "c \<subseteq> -s"
using assms by (simp add: in_components_subset)
with \<open>a \<in> c\<close> have "a \<notin> s" by blast
then have ceq: "c = connected_component_set (- s) a"
by (metis \<open>a \<in> c\<close> cin components_iff connected_component_eq)
then have "bounded (s \<union> connected_component_set (- s) a)"
using \<open>compact s\<close> boc compact_imp_bounded by auto
with bounded_subset_ballD obtain r where "0 < r" and r: "(s \<union> connected_component_set (- s) a) \<subseteq> ball a r"
by blast
{ fix g
assume "continuous_on (s \<union> c) g"
"g ` (s \<union> c) \<subseteq> sphere 0 1"
and [simp]: "\<And>x. x \<in> s \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
then have [simp]: "\<And>x. x \<in> s \<union> c \<Longrightarrow> norm (g x) = 1"
by force
have cb_eq: "cball a r = (s \<union> connected_component_set (- s) a) \<union>
(cball a r - connected_component_set (- s) a)"
using ball_subset_cball [of a r] r by auto
have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
(\<lambda>x. a + r *\<^sub>R g x)"
apply (rule continuous_intros)+
using \<open>continuous_on (s \<union> c) g\<close> ceq by blast
have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
(\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
have 1: "continuous_on (cball a r)
(\<lambda>x. if connected_component (- s) a x
then a + r *\<^sub>R g x
else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
apply (subst cb_eq)
apply (rule continuous_on_cases [OF _ _ cont1 cont2])
using ceq cin
apply (auto intro: closed_Un_complement_component
simp: \<open>closed s\<close> open_Compl open_connected_component)
done
have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
\<subseteq> sphere a r "
using \<open>0 < r\<close> by (force simp: dist_norm ceq)
have "retraction (cball a r) (sphere a r)
(\<lambda>x. if x \<in> connected_component_set (- s) a
then a + r *\<^sub>R g x
else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
using \<open>0 < r\<close>
apply (simp add: retraction_def dist_norm 1 2, safe)
apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \<open>a \<notin> s\<close>)
using r
by (auto simp: dist_norm norm_minus_commute)
then have False
using no_retraction_cball
[OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
of "\<lambda>x. if x \<in> connected_component_set (- s) a
then a + r *\<^sub>R g x
else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
by blast
}
then show ?thesis
by blast
qed
subsection\<open>Absolute retracts, Etc.\<close>
text\<open>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. \<close>
(*This turns out to be sufficient (since any set in
R^n can be embedded as a closed subset of a convex subset of R^{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. -- JRH*)
definition AR :: "'a::topological_space set => bool"
where
"AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
\<longrightarrow> S' retract_of U"
definition ANR :: "'a::topological_space set => bool"
where
"ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
\<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
S' retract_of T)"
definition ENR :: "'a::topological_space set => bool"
where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
text\<open> First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
proposition AR_imp_absolute_extensor:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
and cloUT: "closedin (subtopology euclidean U) T"
obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
proof -
have "aff_dim S < int (DIM('b \<times> real))"
using aff_dim_le_DIM [of S] by simp
then obtain C and S' :: "('b * real) set"
where C: "convex C" "C \<noteq> {}"
and cloCS: "closedin (subtopology euclidean C) S'"
and hom: "S homeomorphic S'"
by (metis that homeomorphic_closedin_convex)
then have "S' retract_of C"
using \<open>AR S\<close> by (simp add: AR_def)
then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> 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 \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
then have contgf: "continuous_on T (g o f)"
by (metis continuous_on_compose contf)
have gfTC: "(g \<circ> f) ` T \<subseteq> C"
proof -
have "g ` S = S'"
by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
qed
obtain f' where f': "continuous_on U f'" "f' ` U \<subseteq> C"
"\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
by (metis Dugundji [OF C cloUT contgf gfTC])
show ?thesis
proof (rule_tac g = "h o r o f'" in that)
show "continuous_on U (h \<circ> r \<circ> f')"
apply (intro continuous_on_compose f')
using continuous_on_subset contr f' apply blast
by (meson \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> continuous_on_subset \<open>f' ` U \<subseteq> C\<close> homeomorphism_def image_mono)
show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
by (fastforce simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> 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 (subtopology euclidean 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' \<subseteq> S"
using hom homeomorphism_def apply blast
apply (metis hom equalityE homeomorphism_def)
done
obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
have [simp]: "S' \<subseteq> 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 o h')"
apply (intro continuous_on_compose h')
apply (meson hom continuous_on_subset h' homeomorphism_cont1)
done
show "(g \<circ> h') ` U \<subseteq> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> 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 \<open>AR S\<close> hom])
using clo closed_closedin by auto
lemma absolute_extensor_imp_AR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
\<And>U T. \<lbrakk>continuous_on T f; f ` T \<subseteq> S;
closedin (subtopology euclidean U) T\<rbrakk>
\<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> 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 (subtopology euclidean 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 \<subseteq> S"
using hom homeomorphism_def apply blast
apply (metis hom equalityE homeomorphism_def)
done
obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
and h'h: "\<forall>x\<in>T. h' x = h x"
using assms [OF h clo] by blast
have [simp]: "T \<subseteq> 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 o h')"
apply (intro continuous_on_compose h')
apply (meson hom continuous_on_subset h' homeomorphism_cont1)
done
show "(g \<circ> h') ` U \<subseteq> T"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>T. (g \<circ> 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 \<longleftrightarrow>
(\<forall>f :: 'a * real \<Rightarrow> 'a.
\<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
closedin (subtopology euclidean U) T \<longrightarrow>
(\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> 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 \<and> closedin (subtopology euclidean 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 \<Longrightarrow> AR S \<longleftrightarrow> AR T"
by (metis AR_homeomorphic_AR homeomorphic_sym)
proposition ANR_imp_absolute_neighbourhood_extensor:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
and cloUT: "closedin (subtopology euclidean U) T"
obtains V g where "T \<subseteq> V" "openin (subtopology euclidean U) V"
"continuous_on V g"
"g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
proof -
have "aff_dim S < int (DIM('b \<times> real))"
using aff_dim_le_DIM [of S] by simp
then obtain C and S' :: "('b * real) set"
where C: "convex C" "C \<noteq> {}"
and cloCS: "closedin (subtopology euclidean C) S'"
and hom: "S homeomorphic S'"
by (metis that homeomorphic_closedin_convex)
then obtain D where opD: "openin (subtopology euclidean C) D" and "S' retract_of D"
using \<open>ANR S\<close> by (auto simp: ANR_def)
then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> 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 \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
then have contgf: "continuous_on T (g o f)"
by (intro continuous_on_compose contf)
have gfTC: "(g \<circ> f) ` T \<subseteq> 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 \<subseteq> C"
and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
by (metis Dugundji [OF C cloUT contgf gfTC])
show ?thesis
proof (rule_tac V = "{x \<in> U. f' x \<in> D}" and g = "h o r o f'" in that)
show "T \<subseteq> {x \<in> U. f' x \<in> D}"
using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
by fastforce
show ope: "openin (subtopology euclidean U) {x \<in> U. f' x \<in> D}"
using \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
have conth: "continuous_on (r ` f' ` {x \<in> U. f' x \<in> D}) h"
apply (rule continuous_on_subset [of S'])
using homeomorphism_def homgh apply blast
using \<open>r ` D \<subseteq> S'\<close> by blast
show "continuous_on {x \<in> U. f' x \<in> D} (h \<circ> r \<circ> f')"
apply (intro continuous_on_compose conth
continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
done
show "(h \<circ> r \<circ> f') ` {x \<in> U. f' x \<in> D} \<subseteq> S"
using \<open>homeomorphism S S' g h\<close> \<open>f' ` U \<subseteq> C\<close> \<open>r ` D \<subseteq> S'\<close>
by (auto simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> 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 (subtopology euclidean U) S'"
obtains V where "openin (subtopology euclidean 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' \<subseteq> S"
using hom homeomorphism_def apply blast
apply (metis hom equalityE homeomorphism_def)
done
from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
obtain V h' where "S' \<subseteq> V" and opUV: "openin (subtopology euclidean U) V"
and h': "continuous_on V h'" "h' ` V \<subseteq> S"
and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
have "S' retract_of V"
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
show "continuous_on V (g o h')"
apply (intro continuous_on_compose h')
apply (meson hom continuous_on_subset h' homeomorphism_cont1)
done
show "(g \<circ> h') ` V \<subseteq> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> 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 \<open>ANR S\<close> hom]
by (metis clo closed_closedin open_openin subtopology_UNIV)
lemma absolute_neighbourhood_extensor_imp_ANR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
\<And>U T. \<lbrakk>continuous_on T f; f ` T \<subseteq> S;
closedin (subtopology euclidean U) T\<rbrakk>
\<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> 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 (subtopology euclidean 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 \<subseteq> S"
using hom homeomorphism_def apply blast
apply (metis hom equalityE homeomorphism_def)
done
obtain V h' where "T \<subseteq> V" and opV: "openin (subtopology euclidean U) V"
and h': "continuous_on V h'" "h' ` V \<subseteq> S"
and h'h: "\<forall>x\<in>T. h' x = h x"
using assms [OF h clo] by blast
have [simp]: "T \<subseteq> U"
using clo closedin_imp_subset by auto
have "T retract_of V"
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
show "continuous_on V (g o h')"
apply (intro continuous_on_compose h')
apply (meson hom continuous_on_subset h' homeomorphism_cont1)
done
show "(g \<circ> h') ` V \<subseteq> T"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>T. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
qed
then show "\<exists>V. openin (subtopology euclidean U) V \<and> T retract_of V"
using opV by blast
qed
lemma ANR_eq_absolute_neighbourhood_extensor:
fixes S :: "'a::euclidean_space set"
shows "ANR S \<longleftrightarrow>
(\<forall>f :: 'a * real \<Rightarrow> 'a.
\<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
closedin (subtopology euclidean U) T \<longrightarrow>
(\<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> 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 (subtopology euclidean U) S"
obtains V where "openin (subtopology euclidean 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 (subtopology euclidean U) S'"
obtains V W
where "openin (subtopology euclidean U) V"
"closedin (subtopology euclidean U) W"
"S' \<subseteq> V" "V \<subseteq> W" "S' retract_of W"
proof -
obtain Z where "openin (subtopology euclidean U) Z" and S'Z: "S' retract_of Z"
by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
then have UUZ: "closedin (subtopology euclidean U) (U - Z)"
by auto
have "S' \<inter> (U - Z) = {}"
using \<open>S' retract_of Z\<close> closedin_retract closedin_subtopology by fastforce
then obtain V W
where "openin (subtopology euclidean U) V"
and "openin (subtopology euclidean U) W"
and "S' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> 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' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset apply fastforce
using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
ultimately show ?thesis
apply (rule_tac V=V and W = "U-W" in that)
using openin_imp_subset apply (force simp:)+
done
qed
lemma ANR_imp_closed_neighbourhood_retract:
fixes S :: "'a::euclidean_space set"
assumes "ANR S" "closedin (subtopology euclidean U) S"
obtains V W where "openin (subtopology euclidean U) V"
"closedin (subtopology euclidean U) W"
"S \<subseteq> V" "V \<subseteq> 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 \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
by (metis ANR_homeomorphic_ANR homeomorphic_sym)
subsection\<open> Analogous properties of ENRs.\<close>
proposition 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' \<subseteq> U"
obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
proof -
obtain X where "open X" "S retract_of X"
using \<open>ENR S\<close> 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 \<open>S retract_of X\<close> \<open>open X\<close> hom by blast
then obtain W where UW: "openin (subtopology euclidean U) W"
and WS': "closedin (subtopology euclidean W) S'"
apply (rule locally_compact_closedin_open)
apply (rename_tac W)
apply (rule_tac W = "U \<inter> W" in that, blast)
by (simp add: \<open>S' \<subseteq> U\<close> 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' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
using Tietze_unbounded [of S' g W] WS' by blast
have "W \<subseteq> U" using UW openin_open by auto
have "S' \<subseteq> W" using WS' closedin_closed by auto
have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
have "S' retract_of {x \<in> W. h x \<in> X}"
proof (simp add: retraction_def retract_of_def, intro exI conjI)
show "S' \<subseteq> {x \<in> W. h x \<in> X}"
using him WS' closedin_imp_subset by blast
show "continuous_on {x \<in> W. h x \<in> X} (f o r o h)"
proof (intro continuous_on_compose)
show "continuous_on {x \<in> W. h x \<in> X} h"
by (metis (no_types) Collect_restrict conth continuous_on_subset)
show "continuous_on (h ` {x \<in> W. h x \<in> X}) r"
proof -
have "h ` {b \<in> W. h b \<in> X} \<subseteq> X"
by blast
then show "continuous_on (h ` {b \<in> W. h b \<in> X}) r"
by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
qed
show "continuous_on (r ` h ` {x \<in> W. h x \<in> X}) f"
apply (rule continuous_on_subset [of S])
using hom homeomorphism_def apply blast
apply clarify
apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
done
qed
show "(f \<circ> r \<circ> h) ` {x \<in> W. h x \<in> X} \<subseteq> S'"
using \<open>retraction X S r\<close> hom
by (auto simp: retraction_def homeomorphism_def)
show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
qed
then show ?thesis
apply (rule_tac V = "{x. x \<in> W \<and> h x \<in> X}" in that)
apply (rule openin_trans [OF _ UW])
using \<open>continuous_on W h\<close> \<open>open X\<close> 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 \<longleftrightarrow> ENR T"
by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
lemma ENR_translation:
fixes S :: "'a::euclidean_space set"
shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
lemma ENR_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
shows "ENR (image f S) \<longleftrightarrow> ENR S"
apply (rule homeomorphic_ENR_iff_ENR)
using assms homeomorphic_sym linear_homeomorphic_image by auto
subsection\<open>Some relations among the concepts\<close>
text\<open>We also relate AR to being a retract of UNIV, which is often a more convenient proxy in the closed case.\<close>
lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
using ANR_def AR_def by fastforce
lemma ENR_imp_ANR:
fixes S :: "'a::euclidean_space set"
shows "ENR S \<Longrightarrow> 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 \<longleftrightarrow> ANR S \<and> 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 \<and> locally compact S"
using ENR_imp_ANR \<open>ENR S\<close> by blast
next
assume "ANR S \<and> 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 \<open>ANR S\<close>
apply (simp add: ANR_def)
apply (drule_tac x=UNIV in spec)
apply (drule_tac x=T in spec)
apply (auto simp: closed_closedin)
apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
done
qed
proposition AR_ANR:
fixes S :: "'a::euclidean_space set"
shows "AR S \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
(is "?lhs = ?rhs")
proof
assume ?lhs
obtain C and S' :: "('a * real) set"
where "convex C" "C \<noteq> {}" "closedin (subtopology euclidean 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 \<open>AR S\<close> 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 \<open>AR S\<close> show ?rhs
apply (auto simp: AR_imp_ANR)
apply (force simp: AR_def)
done
next
assume ?rhs
then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
where conth: "continuous_on ({0..1} \<times> S) h"
and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
and [simp]: "\<And>x. h(0, x) = x"
and [simp]: "\<And>x. h(1, x) = a"
and "ANR S" "S \<noteq> {}"
by (auto simp: contractible_def homotopic_with_def)
then have "a \<in> S"
by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
if f: "continuous_on T f" "f ` T \<subseteq> S"
and WT: "closedin (subtopology euclidean W) T"
for W T and f :: "'a \<times> real \<Rightarrow> 'a"
proof -
obtain U g
where "T \<subseteq> U" and WU: "openin (subtopology euclidean W) U"
and contg: "continuous_on U g"
and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
by auto
have WWU: "closedin (subtopology euclidean W) (W - U)"
using WU closedin_diff by fastforce
moreover have "(W - U) \<inter> T = {}"
using \<open>T \<subseteq> U\<close> by auto
ultimately obtain V V'
where WV': "openin (subtopology euclidean W) V'"
and WV: "openin (subtopology euclidean W) V"
and "W - U \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
using separation_normal_local [of W "W-U" T] WT by blast
then have WVT: "T \<inter> (W - V) = {}"
by auto
have WWV: "closedin (subtopology euclidean W) (W - V)"
using WV closedin_diff by fastforce
obtain j :: " 'a \<times> real \<Rightarrow> real"
where contj: "continuous_on W j"
and j: "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
have Weq: "W = (W - V) \<union> (W - V')"
using \<open>V' \<inter> V = {}\<close> by force
show ?thesis
proof (intro conjI exI)
have *: "continuous_on (W - V') (\<lambda>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 \<open>W - U \<subseteq> V'\<close>)
using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> apply fastforce
done
show "continuous_on W (\<lambda>x. if x \<in> 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)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
proof -
have "j(x, y) \<in> {0..1}"
using j that by blast
moreover have "g(x, y) \<in> S"
using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
ultimately show ?thesis
using hS by blast
qed
with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
by auto
next
show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
using \<open>T \<subseteq> V\<close> 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 o 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 "\<lbrakk>AR T; S retract_of T\<rbrakk> \<Longrightarrow> AR S"
using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce
lemma ENR_retract_of_ENR:
"\<lbrakk>ENR T; S retract_of T\<rbrakk> \<Longrightarrow> ENR S"
by (meson ENR_def retract_of_trans)
lemma retract_of_UNIV:
fixes S :: "'a::euclidean_space set"
shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> 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 [simp]:
fixes S :: "'a::euclidean_space set"
shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
using compact_imp_closed retract_of_UNIV by blast
subsection\<open>More properties of ARs, ANRs and ENRs\<close>
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 "\<lbrakk>convex S; S \<noteq> {}\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> ANR S"
using ANR_empty AR_imp_ANR convex_imp_AR by blast
lemma ENR_convex_closed:
fixes S :: "'a::euclidean_space set"
shows "\<lbrakk>closed S; convex S\<rbrakk> \<Longrightarrow> 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
subsection\<open>ARs closed under union\<close>
lemma AR_closed_Un_local_aux:
fixes U :: "'a::euclidean_space set"
assumes "closedin (subtopology euclidean U) S"
"closedin (subtopology euclidean U) T"
"AR S" "AR T" "AR(S \<inter> T)"
shows "(S \<union> T) retract_of U"
proof -
have "S \<inter> T \<noteq> {}"
using assms AR_def by fastforce
have "S \<subseteq> U" "T \<subseteq> U"
using assms by (auto simp: closedin_imp_subset)
define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
define W where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
have US': "closedin (subtopology euclidean U) S'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
by (simp add: S'_def continuous_intros)
have UT': "closedin (subtopology euclidean U) T'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
by (simp add: T'_def continuous_intros)
have "S \<subseteq> S'"
using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "T \<subseteq> T'"
using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "S \<inter> T \<subseteq> W" "W \<subseteq> U"
using \<open>S \<subseteq> U\<close> by (auto simp: W_def setdist_sing_in_set)
have "(S \<inter> T) retract_of W"
apply (rule AR_imp_absolute_retract [OF \<open>AR(S \<inter> T)\<close>])
apply (simp add: homeomorphic_refl)
apply (rule closedin_subset_trans [of U])
apply (simp_all add: assms closedin_Int \<open>S \<inter> T \<subseteq> W\<close> \<open>W \<subseteq> U\<close>)
done
then obtain r0
where "S \<inter> T \<subseteq> W" and contr0: "continuous_on W r0"
and "r0 ` W \<subseteq> S \<inter> T"
and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
by (auto simp: retract_of_def retraction_def)
have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
using setdist_eq_0_closedin \<open>S \<inter> T \<noteq> {}\<close> assms
by (force simp: W_def setdist_sing_in_set)
have "S' \<inter> T' = W"
by (auto simp: S'_def T'_def W_def)
then have cloUW: "closedin (subtopology euclidean U) W"
using closedin_Int US' UT' by blast
define r where "r \<equiv> \<lambda>x. if x \<in> W then r0 x else x"
have "r ` (W \<union> S) \<subseteq> S" "r ` (W \<union> T) \<subseteq> T"
using \<open>r0 ` W \<subseteq> S \<inter> T\<close> r_def by auto
have contr: "continuous_on (W \<union> (S \<union> T)) r"
unfolding r_def
proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
show "closedin (subtopology euclidean (W \<union> (S \<union> T))) W"
using \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> \<open>closedin (subtopology euclidean U) W\<close> closedin_subset_trans by fastforce
show "closedin (subtopology euclidean (W \<union> (S \<union> T))) (S \<union> T)"
by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
show "\<And>x. x \<in> W \<and> x \<notin> W \<or> x \<in> S \<union> T \<and> x \<in> W \<Longrightarrow> r0 x = x"
by (auto simp: ST)
qed
have cloUWS: "closedin (subtopology euclidean U) (W \<union> S)"
by (simp add: cloUW assms closedin_Un)
obtain g where contg: "continuous_on U g"
and "g ` U \<subseteq> S" and geqr: "\<And>x. x \<in> W \<union> S \<Longrightarrow> g x = r x"
apply (rule AR_imp_absolute_extensor [OF \<open>AR S\<close> _ _ cloUWS])
apply (rule continuous_on_subset [OF contr])
using \<open>r ` (W \<union> S) \<subseteq> S\<close> apply auto
done
have cloUWT: "closedin (subtopology euclidean U) (W \<union> T)"
by (simp add: cloUW assms closedin_Un)
obtain h where conth: "continuous_on U h"
and "h ` U \<subseteq> T" and heqr: "\<And>x. x \<in> W \<union> T \<Longrightarrow> h x = r x"
apply (rule AR_imp_absolute_extensor [OF \<open>AR T\<close> _ _ cloUWT])
apply (rule continuous_on_subset [OF contr])
using \<open>r ` (W \<union> T) \<subseteq> T\<close> apply auto
done
have "U = S' \<union> T'"
by (force simp: S'_def T'_def)
then have cont: "continuous_on U (\<lambda>x. if x \<in> S' then g x else h x)"
apply (rule ssubst)
apply (rule continuous_on_cases_local)
using US' UT' \<open>S' \<inter> T' = W\<close> \<open>U = S' \<union> T'\<close>
contg conth continuous_on_subset geqr heqr apply auto
done
have UST: "(\<lambda>x. if x \<in> S' then g x else h x) ` U \<subseteq> S \<union> T"
using \<open>g ` U \<subseteq> S\<close> \<open>h ` U \<subseteq> T\<close> by auto
show ?thesis
apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
apply (intro conjI cont UST)
by (metis IntI ST Un_iff \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> subsetD geqr heqr r0 r_def)
qed
proposition AR_closed_Un_local:
fixes S :: "'a::euclidean_space set"
assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
and STT: "closedin (subtopology euclidean (S \<union> T)) T"
and "AR S" "AR T" "AR(S \<inter> T)"
shows "AR(S \<union> T)"
proof -
have "C retract_of U"
if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
for U and C :: "('a * real) set"
proof -
obtain f g where hom: "homeomorphism (S \<union> T) C f g"
using hom by (force simp: homeomorphic_def)
have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> 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 (subtopology euclidean U) {x \<in> C. g x \<in> 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 {x \<in> C. g x \<in> S}"
apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
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 {x \<in> C. g x \<in> T}"
apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
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 ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
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 = {x \<in> C. g x \<in> S} \<union> {x \<in> C. g x \<in> 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 "\<lbrakk>closed S; closed T; AR S; AR T; AR (S \<inter> T)\<rbrakk> \<Longrightarrow> AR (S \<union> T)"
by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)
subsection\<open>ANRs closed under union\<close>
lemma ANR_closed_Un_local_aux:
fixes U :: "'a::euclidean_space set"
assumes US: "closedin (subtopology euclidean U) S"
and UT: "closedin (subtopology euclidean U) T"
and "ANR S" "ANR T" "ANR(S \<inter> T)"
obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
proof (cases "S = {} \<or> T = {}")
case True with assms that show ?thesis
by (auto simp: intro: ANR_imp_neighbourhood_retract)
next
case False
then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
have "S \<subseteq> U" "T \<subseteq> U"
using assms by (auto simp: closedin_imp_subset)
define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
define W where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
have cloUS': "closedin (subtopology euclidean U) S'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
by (simp add: S'_def continuous_intros)
have cloUT': "closedin (subtopology euclidean U) T'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
by (simp add: T'_def continuous_intros)
have "S \<subseteq> S'"
using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "T \<subseteq> T'"
using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "S' \<union> T' = U"
by (auto simp: S'_def T'_def)
have "W \<subseteq> S'"
by (simp add: Collect_mono S'_def W_def)
have "W \<subseteq> T'"
by (simp add: Collect_mono T'_def W_def)
have ST_W: "S \<inter> T \<subseteq> W" and "W \<subseteq> U"
using \<open>S \<subseteq> U\<close> by (force simp: W_def setdist_sing_in_set)+
have "S' \<inter> T' = W"
by (auto simp: S'_def T'_def W_def)
then have cloUW: "closedin (subtopology euclidean U) W"
using closedin_Int cloUS' cloUT' by blast
obtain W' W0 where "openin (subtopology euclidean W) W'"
and cloWW0: "closedin (subtopology euclidean W) W0"
and "S \<inter> T \<subseteq> W'" "W' \<subseteq> W0"
and ret: "(S \<inter> T) retract_of W0"
apply (rule ANR_imp_closed_neighbourhood_retract [OF \<open>ANR(S \<inter> T)\<close>])
apply (rule closedin_subset_trans [of U, OF _ ST_W \<open>W \<subseteq> U\<close>])
apply (blast intro: assms)+
done
then obtain U0 where opeUU0: "openin (subtopology euclidean U) U0"
and U0: "S \<inter> T \<subseteq> U0" "U0 \<inter> W \<subseteq> W0"
unfolding openin_open using \<open>W \<subseteq> U\<close> by blast
have "W0 \<subseteq> U"
using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
obtain r0
where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
using ret by (force simp add: retract_of_def retraction_def)
have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
unfolding r_def
proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) W0"
apply (rule closedin_subset_trans [of U])
using cloWW0 cloUW closedin_trans \<open>W0 \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> apply blast+
done
show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) (S \<union> T)"
by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W0 \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
show "\<And>x. x \<in> W0 \<and> x \<notin> W0 \<or> x \<in> S \<union> T \<and> x \<in> W0 \<Longrightarrow> r0 x = x"
using ST cloWW0 closedin_subset by fastforce
qed
have cloS'WS: "closedin (subtopology euclidean S') (W0 \<union> S)"
by (meson closedin_subset_trans US cloUS' \<open>S \<subseteq> S'\<close> \<open>W \<subseteq> S'\<close> cloUW cloWW0
closedin_Un closedin_imp_subset closedin_trans)
obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
and opeSW1: "openin (subtopology euclidean S') W1"
and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
apply (rule continuous_on_subset [OF contr])
apply (blast intro: elim: )+
done
have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0
closedin_Un closedin_imp_subset closedin_trans)
obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
and opeSW2: "openin (subtopology euclidean T') W2"
and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
apply (rule continuous_on_subset [OF contr])
apply (blast intro: elim: )+
done
have "S' \<inter> T' = W"
by (force simp: S'_def T'_def W_def)
obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
using opeSW1 opeSW2 by (force simp add: openin_open)
show ?thesis
proof
have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
((U - T') \<inter> O1 \<union> (U - S') \<inter> O2 \<union> U \<inter> O1 \<inter> O2) - (W - U0)"
using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close>
by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
apply (subst eq)
apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>)
apply simp_all
done
have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
using cloUS' apply (simp add: closedin_closed)
apply (erule ex_forward)
using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
done
have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
using cloUT' apply (simp add: closedin_closed)
apply (erule ex_forward)
using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
done
have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr
apply (auto simp: r_def)
apply fastforce
using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close> by auto
have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and>
(\<forall>x\<in>S \<union> T. r x = x)"
apply (rule_tac x = "\<lambda>x. if x \<in> 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 \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close>
\<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> apply auto
using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> apply (fastforce simp add: geqr heqr)+
done
then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
using \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
by (auto simp add: retract_of_def retraction_def)
qed
qed
proposition ANR_closed_Un_local:
fixes S :: "'a::euclidean_space set"
assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
and STT: "closedin (subtopology euclidean (S \<union> T)) T"
and "ANR S" "ANR T" "ANR(S \<inter> T)"
shows "ANR(S \<union> T)"
proof -
have "\<exists>T. openin (subtopology euclidean U) T \<and> C retract_of T"
if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
for U and C :: "('a * real) set"
proof -
obtain f g where hom: "homeomorphism (S \<union> T) C f g"
using hom by (force simp: homeomorphic_def)
have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> 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 (subtopology euclidean U) {x \<in> C. g x \<in> 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 {x \<in> C. g x \<in> S}"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
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 {x \<in> C. g x \<in> T}"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
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 ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
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 = {x. x \<in> C \<and> g x \<in> S} \<union> {x. x \<in> C \<and> g x \<in> T}"
by auto (metis Un_iff hom homeomorphism_def imageI)
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 "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> 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 (subtopology euclidean T) S"
shows "ANR S"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
and cloUC: "closedin (subtopology euclidean U) C"
have "f ` C \<subseteq> T"
using fim opeTS openin_imp_subset by blast
obtain W g where "C \<subseteq> W"
and UW: "openin (subtopology euclidean U) W"
and contg: "continuous_on W g"
and gim: "g ` W \<subseteq> T"
and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC])
using fim by auto
show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
proof (intro exI conjI)
show "C \<subseteq> {x \<in> W. g x \<in> S}"
using \<open>C \<subseteq> W\<close> fim geq by blast
show "openin (subtopology euclidean U) {x \<in> W. g x \<in> S}"
by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
show "continuous_on {x \<in> W. g x \<in> S} g"
by (blast intro: continuous_on_subset [OF contg])
show "g ` {x \<in> W. g x \<in> S} \<subseteq> S"
using gim by blast
show "\<forall>x\<in>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 (subtopology euclidean 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 (subtopology euclidean 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 (subtopology euclidean 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> ENR(S - {a})"
by (blast intro: ENR_openin openin_delete openin_subtopology_self)
lemma open_imp_ENR: "open S \<Longrightarrow> ENR S"
using ENR_def by blast
lemma open_imp_ANR:
fixes S :: "'a::euclidean_space set"
shows "open S \<Longrightarrow> 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) \<longleftrightarrow> 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) \<longleftrightarrow> 0 \<le> 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) \<longleftrightarrow> cbox a b \<noteq> {}" "AR(box a b) \<longleftrightarrow> box a b \<noteq> {}"
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 \<Longrightarrow> contractible S"
by (simp add: AR_ANR)
lemma ENR_imp_locally_compact:
fixes S :: "'a::euclidean_space set"
shows "ENR S \<Longrightarrow> 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 \<times> real) set"
where "convex U" "U \<noteq> {}"
and UT: "closedin (subtopology euclidean U) T"
and "S homeomorphic T"
apply (rule homeomorphic_closedin_convex [of S])
using aff_dim_le_DIM [of S] apply auto
done
have "locally path_connected T"
by (meson ANR_imp_absolute_neighbourhood_retract \<open>S homeomorphic T\<close> \<open>closedin (subtopology euclidean U) T\<close> \<open>convex U\<close> assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
then have S: "locally path_connected S"
if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
using \<open>S homeomorphic T\<close> 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 \<open>S homeomorphic T\<close> \<open>U \<noteq> {}\<close> 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 \<times> T)"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
and cloUC: "closedin (subtopology euclidean U) C"
have contf1: "continuous_on C (fst \<circ> f)"
by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
obtain W1 g where "C \<subseteq> W1"
and UW1: "openin (subtopology euclidean U) W1"
and contg: "continuous_on W1 g"
and gim: "g ` W1 \<subseteq> S"
and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
using fim apply auto
done
have contf2: "continuous_on C (snd \<circ> f)"
by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
obtain W2 h where "C \<subseteq> W2"
and UW2: "openin (subtopology euclidean U) W2"
and conth: "continuous_on W2 h"
and him: "h ` W2 \<subseteq> T"
and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
using fim apply auto
done
show "\<exists>V g. C \<subseteq> V \<and>
openin (subtopology euclidean U) V \<and>
continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
proof (intro exI conjI)
show "C \<subseteq> W1 \<inter> W2"
by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
show "openin (subtopology euclidean U) (W1 \<inter> W2)"
by (simp add: UW1 UW2 openin_Int)
show "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
show "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
using gim him by blast
show "(\<forall>x\<in>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 \<times> T)"
using assms by (simp add: AR_ANR ANR_Times contractible_Times)
lemma ENR_rel_frontier_convex:
fixes S :: "'a::euclidean_space set"
assumes "bounded S" "convex S"
shows "ENR(rel_frontier S)"
proof (cases "S = {}")
case True then show ?thesis
by simp
next
case False
with assms have "rel_interior S \<noteq> {}"
by (simp add: rel_interior_eq_empty)
then obtain a where a: "a \<in> rel_interior S"
by auto
have ahS: "affine hull S - {a} \<subseteq> {x. closest_point (affine hull S) x \<noteq> a}"
by (auto simp: closest_point_self)
have "rel_frontier S retract_of affine hull S - {a}"
by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull)
also have "... retract_of {x. closest_point (affine hull S) x \<noteq> a}"
apply (simp add: retract_of_def retraction_def ahS)
apply (rule_tac x="closest_point (affine hull S)" in exI)
apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
done
finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
moreover have "openin (subtopology euclidean UNIV) {x \<in> UNIV. closest_point (affine hull S) x \<in> - {a}}"
apply (rule continuous_openin_preimage_gen)
apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
done
ultimately show ?thesis
apply (simp add: ENR_def)
apply (rule_tac x = "{x. x \<in> UNIV \<and>
closest_point (affine hull S) x \<in> (- {a})}" in exI)
apply (simp add: open_openin)
done
qed
lemma ANR_rel_frontier_convex:
fixes S :: "'a::euclidean_space set"
assumes "bounded S" "convex S"
shows "ANR(rel_frontier S)"
by (simp add: ENR_imp_ANR ENR_rel_frontier_convex assms)
(*UNUSED
lemma ENR_Times:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "ENR S" "ENR T" shows "ENR(S \<times> T)"
using assms apply (simp add: ENR_ANR ANR_Times)
thm locally_compact_Times
oops
SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);;
*)
subsection\<open>Borsuk homotopy extension theorem\<close>
text\<open>It's only this late so we can use the concept of retraction,
saying that the domain sets or range set are ENRs.\<close>
theorem Borsuk_homotopy_extension_homotopic:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes cloTS: "closedin (subtopology euclidean T) S"
and anr: "(ANR S \<and> ANR T) \<or> ANR U"
and contf: "continuous_on T f"
and "f ` T \<subseteq> U"
and "homotopic_with (\<lambda>x. True) S U f g"
obtains g' where "homotopic_with (\<lambda>x. True) T U f g'"
"continuous_on T g'" "image g' T \<subseteq> U"
"\<And>x. x \<in> S \<Longrightarrow> g' x = g x"
proof -
have "S \<subseteq> T" using assms closedin_imp_subset by blast
obtain h where conth: "continuous_on ({0..1} \<times> S) h"
and him: "h ` ({0..1} \<times> S) \<subseteq> U"
and [simp]: "\<And>x. h(0, x) = f x" "\<And>x. h(1::real, x) = g x"
using assms by (auto simp: homotopic_with_def)
define h' where "h' \<equiv> \<lambda>z. if snd z \<in> S then h z else (f o snd) z"
define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
have clo0T: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0::real} \<times> T)"
by (simp add: closedin_subtopology_refl closedin_Times)
moreover have cloT1S: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0..1} \<times> S)"
by (simp add: closedin_subtopology_refl closedin_Times assms)
ultimately have clo0TB:"closedin (subtopology euclidean ({0..1} \<times> T)) B"
by (auto simp: B_def)
have cloBS: "closedin (subtopology euclidean B) ({0..1} \<times> S)"
by (metis (no_types) Un_subset_iff B_def closedin_subset_trans [OF cloT1S] clo0TB closedin_imp_subset closedin_self)
moreover have cloBT: "closedin (subtopology euclidean B) ({0} \<times> T)"
using \<open>S \<subseteq> T\<close> closedin_subset_trans [OF clo0T]
by (metis B_def Un_upper1 clo0TB closedin_closed inf_le1)
moreover have "continuous_on ({0} \<times> T) (f \<circ> snd)"
apply (rule continuous_intros)+
apply (simp add: contf)
done
ultimately have conth': "continuous_on B h'"
apply (simp add: h'_def B_def Un_commute [of "{0} \<times> T"])
apply (auto intro!: continuous_on_cases_local conth)
done
have "image h' B \<subseteq> U"
using \<open>f ` T \<subseteq> U\<close> him by (auto simp: h'_def B_def)
obtain V k where "B \<subseteq> V" and opeTV: "openin (subtopology euclidean ({0..1} \<times> T)) V"
and contk: "continuous_on V k" and kim: "k ` V \<subseteq> U"
and keq: "\<And>x. x \<in> B \<Longrightarrow> k x = h' x"
using anr
proof
assume ST: "ANR S \<and> ANR T"
have eq: "({0} \<times> T \<inter> {0..1} \<times> S) = {0::real} \<times> S"
using \<open>S \<subseteq> T\<close> by auto
have "ANR B"
apply (simp add: B_def)
apply (rule ANR_closed_Un_local)
apply (metis cloBT B_def)
apply (metis Un_commute cloBS B_def)
apply (simp_all add: ANR_Times convex_imp_ANR ANR_singleton ST eq)
done
note Vk = that
have *: thesis if "openin (subtopology euclidean ({0..1::real} \<times> T)) V"
"retraction V B r" for V r
using that
apply (clarsimp simp add: retraction_def)
apply (rule Vk [of V "h' o r"], assumption+)
apply (metis continuous_on_compose conth' continuous_on_subset)
using \<open>h' ` B \<subseteq> U\<close> apply force+
done
show thesis
apply (rule ANR_imp_neighbourhood_retract [OF \<open>ANR B\<close> clo0TB])
apply (auto simp: ANR_Times ANR_singleton ST retract_of_def *)
done
next
assume "ANR U"
with ANR_imp_absolute_neighbourhood_extensor \<open>h' ` B \<subseteq> U\<close> clo0TB conth' that
show ?thesis by blast
qed
define S' where "S' \<equiv> {x. \<exists>u::real. u \<in> {0..1} \<and> (u, x::'a) \<in> {0..1} \<times> T - V}"
have "closedin (subtopology euclidean T) S'"
unfolding S'_def
apply (rule closedin_compact_projection, blast)
using closedin_self opeTV by blast
have S'_def: "S' = {x. \<exists>u::real. (u, x::'a) \<in> {0..1} \<times> T - V}"
by (auto simp: S'_def)
have cloTS': "closedin (subtopology euclidean T) S'"
using S'_def \<open>closedin (subtopology euclidean T) S'\<close> by blast
have "S \<inter> S' = {}"
using S'_def B_def \<open>B \<subseteq> V\<close> by force
obtain a :: "'a \<Rightarrow> real" where conta: "continuous_on T a"
and "\<And>x. x \<in> T \<Longrightarrow> a x \<in> closed_segment 1 0"
and a1: "\<And>x. x \<in> S \<Longrightarrow> a x = 1"
and a0: "\<And>x. x \<in> S' \<Longrightarrow> a x = 0"
apply (rule Urysohn_local [OF cloTS cloTS' \<open>S \<inter> S' = {}\<close>, of 1 0], blast)
done
then have ain: "\<And>x. x \<in> T \<Longrightarrow> a x \<in> {0..1}"
using closed_segment_eq_real_ivl by auto
have inV: "(u * a t, t) \<in> V" if "t \<in> T" "0 \<le> u" "u \<le> 1" for t u
proof (rule ccontr)
assume "(u * a t, t) \<notin> V"
with ain [OF \<open>t \<in> T\<close>] have "a t = 0"
apply simp
apply (rule a0)
by (metis (no_types, lifting) Diff_iff S'_def SigmaI atLeastAtMost_iff mem_Collect_eq mult_le_one mult_nonneg_nonneg that)
show False
using B_def \<open>(u * a t, t) \<notin> V\<close> \<open>B \<subseteq> V\<close> \<open>a t = 0\<close> that by auto
qed
show ?thesis
proof
show hom: "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
proof (simp add: homotopic_with, intro exI conjI)
show "continuous_on ({0..1} \<times> T) (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z)))"
apply (intro continuous_on_compose continuous_intros)
apply (rule continuous_on_subset [OF conta], force)
apply (rule continuous_on_subset [OF contk])
apply (force intro: inV)
done
show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) ` ({0..1} \<times> T) \<subseteq> U"
using inV kim by auto
show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (0, x) = f x"
by (simp add: B_def h'_def keq)
show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (1, x) = k (a x, x)"
by auto
qed
show "continuous_on T (\<lambda>x. k (a x, x))"
using hom homotopic_with_imp_continuous by blast
show "(\<lambda>x. k (a x, x)) ` T \<subseteq> U"
proof clarify
fix t
assume "t \<in> T"
show "k (a t, t) \<in> U"
by (metis \<open>t \<in> T\<close> image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1)
qed
show "\<And>x. x \<in> S \<Longrightarrow> k (a x, x) = g x"
by (simp add: B_def a1 h'_def keq)
qed
qed
corollary nullhomotopic_into_ANR_extension:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "closed S"
and contf: "continuous_on S f"
and "ANR T"
and fim: "f ` S \<subseteq> T"
and "S \<noteq> {}"
shows "(\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
by (blast intro: homotopic_with_symD elim: )
have "closedin (subtopology euclidean UNIV) S"
using \<open>closed S\<close> closed_closedin by fastforce
then obtain g where "continuous_on UNIV g" "range g \<subseteq> T"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
apply (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ c, where T=UNIV])
using \<open>ANR T\<close> \<open>S \<noteq> {}\<close> c homotopic_with_imp_subset1 apply fastforce+
done
then show ?rhs by blast
next
assume ?rhs
then obtain g where "continuous_on UNIV g" "range g \<subseteq> T" "\<And>x. x\<in>S \<Longrightarrow> g x = f x"
by blast
then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
then show ?lhs
apply (rule_tac x="c" in exI)
apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
apply (rule homotopic_with_subset_left)
apply (auto simp add: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
done
qed
corollary nullhomotopic_into_rel_frontier_extension:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "closed S"
and contf: "continuous_on S f"
and "convex T" "bounded T"
and fim: "f ` S \<subseteq> rel_frontier T"
and "S \<noteq> {}"
shows "(\<exists>c. homotopic_with (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
corollary nullhomotopic_into_sphere_extension:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "closed S" and contf: "continuous_on S f"
and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
shows "((\<exists>c. homotopic_with (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> sphere a r \<and> (\<forall>x \<in> S. g x = f x)))"
(is "?lhs = ?rhs")
proof (cases "r = 0")
case True with fim show ?thesis
apply (auto simp: )
using fim continuous_on_const apply fastforce
by (metis contf contractible_sing nullhomotopic_into_contractible)
next
case False
then have eq: "sphere a r = rel_frontier (cball a r)" by simp
show ?thesis
using fim unfolding eq
apply (rule nullhomotopic_into_rel_frontier_extension [OF \<open>closed S\<close> contf convex_cball bounded_cball])
apply (rule \<open>S \<noteq> {}\<close>)
done
qed
proposition Borsuk_map_essential_bounded_component:
fixes a :: "'a :: euclidean_space"
assumes "compact S" and "a \<notin> S"
shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
~(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
(is "?lhs = ?rhs")
proof (cases "S = {}")
case True then show ?thesis
by simp
next
case False
have "closed S" "bounded S"
using \<open>compact S\<close> compact_eq_bounded_closed by auto
have s01: "(\<lambda>x. (x - a) /\<^sub>R norm (x - a)) ` S \<subseteq> sphere 0 1"
using \<open>a \<notin> S\<close> by clarsimp (metis dist_eq_0_iff dist_norm mult.commute right_inverse)
have aincc: "a \<in> connected_component_set (- S) a"
by (simp add: \<open>a \<notin> S\<close>)
obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
using bounded_subset_ballD \<open>bounded S\<close> by blast
have "~ ?rhs \<longleftrightarrow> ~ ?lhs"
proof
assume notr: "~ ?rhs"
have nog: "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
(\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
if "bounded (connected_component_set (- S) a)"
apply (rule non_extensible_Borsuk_map [OF \<open>compact S\<close> componentsI _ aincc])
using \<open>a \<notin> S\<close> that by auto
obtain g where "range g \<subseteq> sphere 0 1" "continuous_on UNIV g"
"\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
using notr
by (auto simp add: nullhomotopic_into_sphere_extension
[OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
with \<open>a \<notin> S\<close> show "~ ?lhs"
apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
apply (drule_tac x="g" in spec)
using continuous_on_subset by fastforce
next
assume "~ ?lhs"
then obtain b where b: "b \<in> connected_component_set (- S) a" and "r \<le> norm b"
using bounded_iff linear by blast
then have bnot: "b \<notin> ball 0 r"
by simp
have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
(\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
apply (rule Borsuk_maps_homotopic_in_path_component)
using \<open>closed S\<close> b open_Compl open_path_connected_component apply fastforce
done
moreover
obtain c where "homotopic_with (\<lambda>x. True) (ball 0 r) (sphere 0 1)
(\<lambda>x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\<lambda>x. c)"
proof (rule nullhomotopic_from_contractible)
show "contractible (ball (0::'a) r)"
by (metis convex_imp_contractible convex_ball)
show "continuous_on (ball 0 r) (\<lambda>x. inverse(norm (x - b)) *\<^sub>R (x - b))"
by (rule continuous_on_Borsuk_map [OF bnot])
show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \<subseteq> sphere 0 1"
using bnot Borsuk_map_into_sphere by blast
qed blast
ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
by (meson homotopic_with_subset_left homotopic_with_trans r)
then show "~ ?rhs"
by blast
qed
then show ?thesis by blast
qed
end