--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Jul 17 21:41:14 2023 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Jul 17 21:49:58 2023 +0100
@@ -22,40 +22,39 @@
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 image_subset_iff_funcset)
-apply (rule_tac x="r a" in exI)
-apply (rule_tac x="r \<circ> h" in exI)
-apply (intro conjI continuous_intros continuous_on_compose)
-apply (erule continuous_on_subset | force)+
-done
+ shows "contractible S"
+ using assms
+ apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
+ apply (rule_tac x="r a" in exI)
+ apply (rule_tac x="r \<circ> h" in exI)
+ apply (intro conjI continuous_intros continuous_on_compose)
+ apply (erule continuous_on_subset | force)+
+ done
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 elim!: continuous_on_subset)+
-done
+ "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
+ apply (simp add: retract_of_def retraction_def Pi_iff, clarify)
+ apply (rule simply_connected_retraction_gen)
+ apply (force elim!: continuous_on_subset)+
+ done
lemma retract_of_homotopically_trivial:
assumes ts: "T retract_of S"
- and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
- continuous_on U g; g ` U \<subseteq> S\<rbrakk>
+ and hom: "\<And>f g. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S;
+ continuous_on U g; g \<in> U \<rightarrow> S\<rbrakk>
\<Longrightarrow> homotopic_with_canon (\<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"
+ and "continuous_on U f" "f \<in> U \<rightarrow> T"
+ and "continuous_on U g" "g \<in> U \<rightarrow> T"
shows "homotopic_with_canon (\<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"
+ obtain r where "r \<in> S \<rightarrow> 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)
+ unfolding Retracts_def using continuous_on_id by blast
then show ?thesis
apply (rule Retracts.homotopically_trivial_retraction_gen)
using assms
@@ -65,16 +64,15 @@
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>
+ and hom: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
- and "continuous_on U f" "f ` U \<subseteq> T"
+ and "continuous_on U f" "f \<in> U \<rightarrow> T"
obtains c where "homotopic_with_canon (\<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"
+ obtain r where "r \<in> S \<rightarrow> 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)
+ unfolding Retracts_def by fastforce
then show ?thesis
apply (rule Retracts.homotopically_trivial_retraction_null_gen)
apply (rule TrueI refl assms that | assumption)+
@@ -92,25 +90,24 @@
by (metis locally_compact_closedin closedin_retract)
lemma homotopic_into_retract:
- "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
+ "\<lbrakk>f \<in> S \<rightarrow> T; g \<in> S \<rightarrow> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
\<Longrightarrow> homotopic_with_canon (\<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 \<circ> h" in exI)
-apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
-done
+ apply (subst (asm) homotopic_with_def)
+ apply (simp add: homotopic_with retract_of_def retraction_def Pi_iff, clarify)
+ apply (rule_tac x="r \<circ> h" in exI)
+ by (smt (verit, ccfv_SIG) comp_def continuous_on_compose continuous_on_subset image_subset_iff)
lemma retract_of_locally_connected:
assumes "locally connected T" "S retract_of T"
shows "locally connected S"
using assms
- by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
+ by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
lemma retract_of_locally_path_connected:
assumes "locally path_connected T" "S retract_of T"
shows "locally path_connected S"
using assms
- by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
+ by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
text \<open>A few simple lemmas about deformation retracts\<close>
@@ -133,7 +130,7 @@
lemma deformation_retract:
fixes S :: "'a::euclidean_space set"
shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
- T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
+ T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f \<in> S \<rightarrow> T)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -147,7 +144,7 @@
apply (rule homotopic_with_trans, assumption)
apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
- apply (auto simp: homotopic_with_sym)
+ apply (auto simp: homotopic_with_sym Pi_iff)
done
qed
@@ -161,10 +158,10 @@
moreover have "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
using assms
by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
- moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
+ moreover have "(\<lambda>x. a) \<in> S \<rightarrow> {a}"
by (simp add: image_subsetI)
ultimately show ?thesis
- using that deformation_retract by metis
+ by (metis that deformation_retract)
qed
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jul 17 21:41:14 2023 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jul 17 21:49:58 2023 +0100
@@ -17,9 +17,8 @@
lemma interval_bij_affine:
"interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
(\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
- by (auto simp add: interval_bij_def sum.distrib [symmetric] scaleR_add_left [symmetric]
- fun_eq_iff intro!: sum.cong)
- (simp add: algebra_simps diff_divide_distrib [symmetric])
+ by (simp add: interval_bij_def algebra_simps add_divide_distrib diff_divide_distrib flip: sum.distrib scaleR_add_left)
+
lemma continuous_interval_bij:
fixes a b :: "'a::euclidean_space"
@@ -27,38 +26,22 @@
by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)
lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
- apply(rule continuous_at_imp_continuous_on)
- apply (rule, rule continuous_interval_bij)
- done
+ by (metis continuous_at_imp_continuous_on continuous_interval_bij)
lemma in_interval_interval_bij:
fixes a b u v x :: "'a::euclidean_space"
assumes "x \<in> cbox a b"
and "cbox u v \<noteq> {}"
shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
- apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
- apply safe
proof -
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "cbox a b \<noteq> {}"
- using assms by auto
- with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
- using assms(2) by (auto simp add: box_eq_empty)
- have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
- using assms(1)[unfolded mem_box] using i by auto
- have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
- using * x by auto
- then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
- using * by auto
- have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
- apply (rule mult_right_mono)
- unfolding divide_le_eq_1
- using * x
- apply auto
- done
- then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
- using * by auto
+ have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
+ by (smt (verit) assms box_ne_empty(1) divide_nonneg_nonneg mem_box(2) mult_nonneg_nonneg)
+ moreover
+ have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
+ apply (simp add: divide_simps algebra_simps)
+ by (smt (verit, best) assms box_ne_empty(1) left_diff_distrib mem_box(2) mult.commute mult_left_mono)
+ ultimately show ?thesis
+ by (force simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis)
qed
lemma interval_bij_bij:
@@ -107,9 +90,9 @@
where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
define negatex :: "real^2 \<Rightarrow> real^2"
where "negatex x = (vector [-(x$1), x$2])" for x
- have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
+ have inf_nega: "\<And>z::real^2. infnorm (negatex z) = infnorm z"
unfolding negatex_def infnorm_2 vector_2 by auto
- have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
+ have inf_eq1: "\<And>z. z \<noteq> 0 \<Longrightarrow> infnorm (sqprojection z) = 1"
unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
by (simp add: real_abs_infnorm infnorm_eq_0)
let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
@@ -128,75 +111,59 @@
"x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
unfolding image_iff ..
then have "x \<noteq> 0"
- using as[of "w$1" "w$2"]
- unfolding mem_box_cart atLeastAtMost_iff
- by auto
+ using as[of "w$1" "w$2"] by (auto simp: mem_box_cart atLeastAtMost_iff)
} note x0 = this
- have 1: "box (- 1) (1::real^2) \<noteq> {}"
- unfolding interval_eq_empty_cart by auto
- have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
- for i x y c
- using exhaust_2 [of i] by (auto simp: negatex_def)
- then have "bounded_linear negatex"
- by (simp add: bounded_linearI' vec_eq_iff)
- then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
- apply (intro continuous_intros continuous_on_component)
- unfolding * sqprojection_def
- apply (intro assms continuous_intros)+
- apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
- done
- have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
- unfolding subset_eq
- proof (rule, goal_cases)
- case (1 x)
- then obtain y :: "real^2" where y:
- "y \<in> cbox (- 1) 1"
- "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
- unfolding image_iff ..
- have "?F y \<noteq> 0"
- by (rule x0) (use y in auto)
- then have *: "infnorm (sqprojection (?F y)) = 1"
- unfolding y o_def
- by - (rule lem2[rule_format])
- have inf1: "infnorm x = 1"
- unfolding *[symmetric] y o_def
- by (rule lem1[rule_format])
- show "x \<in> cbox (-1) 1"
- unfolding mem_box_cart interval_cbox_cart infnorm_2
- proof
- fix i
- show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
- using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
- qed
- qed
+ let ?CB11 = "cbox (- 1) (1::real^2)"
obtain x :: "real^2" where x:
"x \<in> cbox (- 1) 1"
"(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
- apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
- apply (rule compact_cbox convex_box)+
- unfolding interior_cbox image_subset_iff_funcset [symmetric]
- apply (rule 1 2 3)+
- apply blast
- done
+ proof (rule brouwer_weak[of ?CB11 "negatex \<circ> sqprojection \<circ> ?F"])
+ show "compact ?CB11" "convex ?CB11"
+ by (rule compact_cbox convex_box)+
+ have "box (- 1) (1::real^2) \<noteq> {}"
+ unfolding interval_eq_empty_cart by auto
+ then show "interior ?CB11 \<noteq> {}"
+ by simp
+ have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
+ for i x y c
+ using exhaust_2 [of i] by (auto simp: negatex_def)
+ then have "bounded_linear negatex"
+ by (simp add: bounded_linearI' vec_eq_iff)
+ then show "continuous_on ?CB11 (negatex \<circ> sqprojection \<circ> ?F)"
+ unfolding sqprojection_def
+ apply (intro continuous_intros continuous_on_component | use * assms in presburger)+
+ apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
+ done
+ have "(negatex \<circ> sqprojection \<circ> ?F) ` ?CB11 \<subseteq> ?CB11"
+ proof clarsimp
+ fix y :: "real^2"
+ assume y: "y \<in> ?CB11"
+ have "?F y \<noteq> 0"
+ by (rule x0) (use y in auto)
+ then have *: "infnorm (sqprojection (?F y)) = 1"
+ using inf_eq1 by blast
+ show "negatex (sqprojection (f (y $ 1) - g (y $ 2))) \<in> cbox (-1) 1"
+ unfolding mem_box_cart interval_cbox_cart infnorm_2
+ by (smt (verit, del_insts) "*" component_le_infnorm_cart inf_nega neg_one_index o_apply one_index)
+ qed
+ then show "negatex \<circ> sqprojection \<circ> ?F \<in> ?CB11 \<rightarrow> ?CB11"
+ by blast
+ qed
have "?F x \<noteq> 0"
by (rule x0) (use x in auto)
then have *: "infnorm (sqprojection (?F x)) = 1"
- unfolding o_def
- by (rule lem2[rule_format])
+ using inf_eq1 by blast
have nx: "infnorm x = 1"
- apply (subst x(2)[symmetric])
- unfolding *[symmetric] o_def
- apply (rule lem1[rule_format])
- done
+ by (metis (no_types, lifting) "*" inf_nega o_apply x(2))
have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i
proof -
- have "inverse (infnorm x) > 0"
+ have *: "inverse (infnorm x) > 0"
by (simp add: infnorm_pos_lt that)
then show "(0 < sqprojection x $ i) = (0 < x $ i)"
- and "(sqprojection x $ i < 0) = (x $ i < 0)"
- unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
- unfolding zero_less_mult_iff mult_less_0_iff
- by (auto simp add: field_simps)
+ by (simp add: sqprojection_def zero_less_mult_iff)
+ show "(sqprojection x $ i < 0) = (x $ i < 0)"
+ unfolding sqprojection_def
+ by (metis * pos_less_divideR_eq scaleR_zero_right vector_scaleR_component)
qed
have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
using x(1) unfolding mem_box_cart by auto
@@ -210,8 +177,7 @@
then have *: "f (x $ 1) $ 1 = - 1"
using assms(5) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
- using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
- by (auto simp: negatex_def 1)
+ by (smt (verit) "1" negatex_def o_apply vector_2(1) x(2))
moreover
from x1 have "g (x $ 2) \<in> cbox (-1) 1"
using assms(2) by blast
@@ -223,8 +189,7 @@
then have *: "f (x $ 1) $ 1 = 1"
using assms(6) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
- using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
- by (auto simp: negatex_def)
+ by (smt (verit) "2" negatex_def o_apply vector_2(1) x(2) zero_less_one)
moreover have "g (x $ 2) \<in> cbox (-1) 1"
using assms(2) x1 by blast
ultimately show False
@@ -234,26 +199,23 @@
case 3
then have *: "g (x $ 2) $ 2 = - 1"
using assms(7) by auto
- have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
- using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
- moreover
- from x1 have "f (x $ 1) \<in> cbox (-1) 1"
+ moreover have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
+ by (smt (verit, ccfv_SIG) "3" negatex_def o_apply vector_2(2) x(2))
+ moreover from x1 have "f (x $ 1) \<in> cbox (-1) 1"
using assms(1) by blast
ultimately show False
- unfolding iff[OF nz] vector_component_simps * mem_box_cart
- by (erule_tac x=2 in allE) auto
+ by (smt (verit, del_insts) iff(2) mem_box_cart(2) neg_one_index nz vector_minus_component)
next
case 4
then have *: "g (x $ 2) $ 2 = 1"
using assms(8) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
- using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
+ by (smt (verit, best) "4" negatex_def o_apply vector_2(2) x(2))
moreover
from x1 have "f (x $ 1) \<in> cbox (-1) 1"
using assms(1) by blast
ultimately show False
- unfolding iff[OF nz] vector_component_simps * mem_box_cart
- by (erule_tac x=2 in allE) auto
+ by (smt (verit) "*" iff(1) mem_box_cart(2) nz one_index vector_minus_component)
qed
qed
@@ -269,7 +231,7 @@
and "(pathfinish g)$2 = 1"
obtains z where "z \<in> path_image f" and "z \<in> path_image g"
proof -
- note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
+ note assms = assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
unfolding iscale_def by auto
@@ -279,38 +241,27 @@
using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
have *: "continuous_on {- 1..1} iscale"
unfolding iscale_def by (rule continuous_intros)+
- show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
- apply -
- apply (rule_tac[!] continuous_on_compose[OF *])
- apply (rule_tac[!] continuous_on_subset[OF _ isc])
- apply (rule assms)+
- done
+ show "continuous_on {- 1..1} (f \<circ> iscale)"
+ using "*" assms(1) continuous_on_compose continuous_on_subset isc by blast
+ show "continuous_on {- 1..1} (g \<circ> iscale)"
+ by (meson "*" assms(2) continuous_on_compose continuous_on_subset isc)
have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
unfolding vec_eq_iff by auto
show "(f \<circ> iscale) (- 1) $ 1 = - 1"
and "(f \<circ> iscale) 1 $ 1 = 1"
and "(g \<circ> iscale) (- 1) $ 2 = -1"
and "(g \<circ> iscale) 1 $ 2 = 1"
- unfolding o_def iscale_def
- using assms
- by (auto simp add: *)
+ unfolding o_def iscale_def using assms by (auto simp add: *)
qed
- then obtain s t where st:
- "s \<in> {- 1..1}"
- "t \<in> {- 1..1}"
- "(f \<circ> iscale) s = (g \<circ> iscale) t"
+ then obtain s t where st: "s \<in> {- 1..1}" "t \<in> {- 1..1}" "(f \<circ> iscale) s = (g \<circ> iscale) t"
by auto
show thesis
- apply (rule_tac z = "f (iscale s)" in that)
- using st
- unfolding o_def path_image_def image_iff
- apply -
- apply (rule_tac x="iscale s" in bexI)
- prefer 3
- apply (rule_tac x="iscale t" in bexI)
- using isc[unfolded subset_eq, rule_format]
- apply auto
- done
+ proof
+ show "f (iscale s) \<in> path_image f"
+ by (metis image_eqI image_subset_iff isc path_image_def st(1))
+ show "f (iscale s) \<in> path_image g"
+ by (metis comp_def image_eqI image_subset_iff isc path_image_def st(2) st(3))
+ qed
qed
theorem fashoda:
@@ -339,66 +290,39 @@
next
assume as: "a$1 = b$1"
have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
- apply (rule connected_ivt_component_cart)
- apply (rule connected_path_image assms)+
- apply (rule pathstart_in_path_image)
- apply (rule pathfinish_in_path_image)
- unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
- unfolding pathstart_def
- apply (auto simp add: less_eq_vec_def mem_box_cart)
- done
+ proof (rule connected_ivt_component_cart)
+ show "pathstart g $ 2 \<le> pathstart f $ 2"
+ by (metis assms(3) assms(7) mem_box_cart(2) pathstart_in_path_image subset_iff)
+ show "pathstart f $ 2 \<le> pathfinish g $ 2"
+ by (metis assms(3) assms(8) in_mono mem_box_cart(2) pathstart_in_path_image)
+ show "connected (path_image g)"
+ using assms(2) by blast
+ qed (auto simp: path_defs)
then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
have "z \<in> cbox a b"
- using z(1) assms(4)
- unfolding path_image_def
- by blast
+ using assms(4) z(1) by blast
then have "z = f 0"
- unfolding vec_eq_iff forall_2
- unfolding z(2) pathstart_def
- using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
- unfolding mem_box_cart
- apply (erule_tac x=1 in allE)
- using as
- apply auto
- done
+ by (smt (verit) as assms(5) exhaust_2 mem_box_cart(2) nle_le pathstart_def vec_eq_iff z(2))
then show thesis
- apply -
- apply (rule that[OF _ z(1)])
- unfolding path_image_def
- apply auto
- done
+ by (metis path_defs(2) pathstart_in_path_image that z(1))
next
assume as: "a$2 = b$2"
have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
- apply (rule connected_ivt_component_cart)
- apply (rule connected_path_image assms)+
- apply (rule pathstart_in_path_image)
- apply (rule pathfinish_in_path_image)
- unfolding assms
- using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
- unfolding pathstart_def
- apply (auto simp add: less_eq_vec_def mem_box_cart)
- done
+ proof (rule connected_ivt_component_cart)
+ show "pathstart f $ 1 \<le> pathstart g $ 1"
+ using assms(4) assms(5) mem_box_cart(2) by fastforce
+ show "pathstart g $ 1 \<le> pathfinish f $ 1"
+ using assms(4) assms(6) mem_box_cart(2) pathstart_in_path_image by fastforce
+ show "connected (path_image f)"
+ by (simp add: assms(1) connected_path_image)
+ qed (auto simp: path_defs)
then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
have "z \<in> cbox a b"
- using z(1) assms(3)
- unfolding path_image_def
- by blast
+ using assms(3) z(1) by auto
then have "z = g 0"
- unfolding vec_eq_iff forall_2
- unfolding z(2) pathstart_def
- using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
- unfolding mem_box_cart
- apply (erule_tac x=2 in allE)
- using as
- apply auto
- done
+ by (smt (verit) as assms(7) exhaust_2 mem_box_cart(2) pathstart_def vec_eq_iff z(2))
then show thesis
- apply -
- apply (rule that[OF z(1)])
- unfolding path_image_def
- apply auto
- done
+ by (metis path_defs(2) pathstart_in_path_image that z(1))
next
assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
@@ -406,61 +330,30 @@
obtain z :: "real^2" where z:
"z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
"z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
- apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
- unfolding path_def path_image_def pathstart_def pathfinish_def
- apply (rule_tac[1-2] continuous_on_compose)
- apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
- unfolding subset_eq
- apply(rule_tac[1-2] ballI)
- proof -
- fix x
- assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
- then obtain y where y:
- "y \<in> {0..1}"
- "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
- unfolding image_iff ..
- show "x \<in> cbox (- 1) 1"
- unfolding y o_def
- apply (rule in_interval_interval_bij)
- using y(1)
- using assms(3)[unfolded path_image_def subset_eq] int_nem
- apply auto
- done
- next
- fix x
- assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
- then obtain y where y:
- "y \<in> {0..1}"
- "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
- unfolding image_iff ..
- show "x \<in> cbox (- 1) 1"
- unfolding y o_def
- apply (rule in_interval_interval_bij)
- using y(1)
- using assms(4)[unfolded path_image_def subset_eq] int_nem
- apply auto
- done
- next
- show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
- and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
- and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
- and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
+ proof (rule fashoda_unit_path)
+ show "path (interval_bij (a, b) (- 1, 1) \<circ> f)"
+ by (meson assms(1) continuous_on_interval_bij path_continuous_image)
+ show "path (interval_bij (a, b) (- 1, 1) \<circ> g)"
+ by (meson assms(2) continuous_on_interval_bij path_continuous_image)
+ show "path_image (interval_bij (a, b) (- 1, 1) \<circ> f) \<subseteq> cbox (- 1) 1"
+ using assms(3)
+ by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
+ show "path_image (interval_bij (a, b) (- 1, 1) \<circ> g) \<subseteq> cbox (- 1) 1"
+ using assms(4)
+ by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
+ show "pathstart (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = - 1"
+ "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = 1"
+ "pathstart (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = - 1"
+ "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = 1"
using assms as
by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
(simp_all add: inner_axis)
- qed
- from z(1) obtain zf where zf:
- "zf \<in> {0..1}"
- "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
- unfolding image_iff ..
- from z(2) obtain zg where zg:
- "zg \<in> {0..1}"
- "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
- unfolding image_iff ..
+ qed (auto simp: path_defs)
+ then obtain zf zg where zf: "zf \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
+ and zg: "zg \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
+ by blast
have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
- unfolding forall_2
- using as
- by auto
+ unfolding forall_2 using as by auto
show thesis
proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
show "interval_bij (- 1, 1) (a, b) z \<in> path_image f"
@@ -493,62 +386,43 @@
then obtain u where u:
"x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
"x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
- "0 \<le> u"
- "u \<le> 1"
+ "0 \<le> u" "u \<le> 1"
by blast
{ fix b a
assume "b + u * a > a + u * b"
then have "(1 - u) * b > (1 - u) * a"
by (auto simp add:field_simps)
then have "b \<ge> a"
- apply (drule_tac mult_left_less_imp_less)
- using u
- apply auto
- done
+ using not_less_iff_gr_or_eq u(4) by fastforce
then have "u * a \<le> u * b"
- apply -
- apply (rule mult_left_mono[OF _ u(3)])
- using u(3-4)
- apply (auto simp add: field_simps)
- done
- } note * = this
- {
- fix a b
+ by (simp add: mult_left_mono u(3))
+ }
+ moreover
+ { fix a b
assume "u * b > u * a"
then have "(1 - u) * a \<le> (1 - u) * b"
- apply -
- apply (rule mult_left_mono)
- apply (drule mult_left_less_imp_less)
- using u
- apply auto
- done
+ using less_eq_real_def u(3) u(4) by force
then have "a + u * b \<le> b + u * a"
by (auto simp add: field_simps)
- } note ** = this
- then show ?R
- unfolding u assms
- using u
- by (auto simp add:field_simps not_le intro: * **)
+ } ultimately show ?R
+ by (force simp add: u assms field_simps not_le)
}
{
assume ?R
then show ?L
proof (cases "x$2 = b$2")
case True
- then show ?L
- apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
- unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps)
- done
+ with \<open>?R\<close> show ?L
+ by (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) (auto simp add: field_simps)
next
case False
- then show ?L
- apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
- unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps)
- done
+ with \<open>?R\<close> show ?L
+ by (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) (auto simp add: field_simps)
qed
}
qed
+text \<open>Essentially duplicate proof that could be done by swapping co-ordinates\<close>
lemma segment_horizontal:
fixes a :: "real^2"
assumes "a$2 = b$2"
@@ -569,63 +443,38 @@
then obtain u where u:
"x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
"x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
- "0 \<le> u"
- "u \<le> 1"
+ "0 \<le> u" "u \<le> 1"
by blast
- {
- fix b a
+ { fix b a
assume "b + u * a > a + u * b"
then have "(1 - u) * b > (1 - u) * a"
by (auto simp add: field_simps)
then have "b \<ge> a"
- apply (drule_tac mult_left_less_imp_less)
- using u
- apply auto
- done
+ by (smt (verit, best) mult_left_mono u(4))
then have "u * a \<le> u * b"
- apply -
- apply (rule mult_left_mono[OF _ u(3)])
- using u(3-4)
- apply (auto simp add: field_simps)
- done
- } note * = this
- {
- fix a b
+ by (simp add: mult_left_mono u(3))
+ }
+ moreover
+ { fix a b
assume "u * b > u * a"
then have "(1 - u) * a \<le> (1 - u) * b"
- apply -
- apply (rule mult_left_mono)
- apply (drule mult_left_less_imp_less)
- using u
- apply auto
- done
+ using less_eq_real_def u(3) u(4) by force
then have "a + u * b \<le> b + u * a"
by (auto simp add: field_simps)
- } note ** = this
- then show ?R
- unfolding u assms
- using u
- by (auto simp add: field_simps not_le intro: * **)
+ }
+ ultimately show ?R
+ by (force simp add: u assms field_simps not_le intro: )
}
- {
- assume ?R
+ { assume ?R
then show ?L
proof (cases "x$1 = b$1")
case True
- then show ?L
- apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
- unfolding assms True
- using \<open>?R\<close>
- apply (auto simp add: field_simps)
- done
+ with \<open>?R\<close> show ?L
+ by (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) (auto simp add: field_simps)
next
case False
- then show ?L
- apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
- unfolding assms
- using \<open>?R\<close>
- apply (auto simp add: field_simps)
- done
+ with \<open>?R\<close> show ?L
+ by (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) (auto simp add: field_simps)
qed
}
qed
@@ -726,9 +575,7 @@
then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
unfolding mem_box_cart forall_2 by auto
then have "z$1 \<noteq> pathfinish f$1"
- using prems(2)
- using assms ab
- by (auto simp add: field_simps)
+ using assms(10) assms(11) prems(2) by auto
moreover have "pathstart f \<in> cbox a b"
using assms(3) pathstart_in_path_image[of f]
by auto
@@ -766,7 +613,7 @@
with z' show "z \<in> path_image f"
using z(1)
unfolding Un_iff mem_box_cart forall_2
- by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
+ using assms(5) assms(6) segment_horizontal segment_vertical by auto
have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
z = pathstart g \<or> z = pathfinish g"
unfolding vec_eq_iff forall_2 assms
@@ -774,7 +621,7 @@
with z' show "z \<in> path_image g"
using z(2)
unfolding Un_iff mem_box_cart forall_2
- by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
+ using assms(7) assms(8) segment_horizontal segment_vertical by auto
qed
qed
--- a/src/HOL/Analysis/Homotopy.thy Mon Jul 17 21:41:14 2023 +0200
+++ b/src/HOL/Analysis/Homotopy.thy Mon Jul 17 21:49:58 2023 +0100
@@ -2971,7 +2971,7 @@
assumes S: "subspace S"
and T: "subspace T"
and d: "dim S \<le> dim T"
- obtains f where "linear f" "f ` S \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+ obtains f where "linear f" "f \<in> S \<rightarrow> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
proof -
obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
@@ -3011,7 +3011,7 @@
by (simp add: norm_eq_sqrt_inner)
qed
then show ?thesis
- by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
+ by (meson \<open>f ` S \<subseteq> T\<close> \<open>linear f\<close> image_subset_iff_funcset that)
qed
proposition isometries_subspaces:
@@ -3190,36 +3190,36 @@
assumes conth: "continuous_on S h"
and imh: "h ` S = t"
and contk: "continuous_on t k"
- and imk: "k ` t \<subseteq> S"
+ and imk: "k \<in> t \<rightarrow> S"
and idhk: "\<And>y. y \<in> t \<Longrightarrow> h(k y) = y"
begin
lemma homotopically_trivial_retraction_gen:
- assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
- and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+ assumes P: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+ and Q: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
- and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f;
- continuous_on U g; g ` U \<subseteq> S; P g\<rbrakk>
+ and hom: "\<And>f g. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f;
+ continuous_on U g; g \<in> U \<rightarrow> S; P g\<rbrakk>
\<Longrightarrow> homotopic_with_canon P U S f g"
- and contf: "continuous_on U f" and imf: "f ` U \<subseteq> t" and Qf: "Q f"
- and contg: "continuous_on U g" and img: "g ` U \<subseteq> t" and Qg: "Q g"
+ and contf: "continuous_on U f" and imf: "f \<in> U \<rightarrow> t" and Qf: "Q f"
+ and contg: "continuous_on U g" and img: "g \<in> U \<rightarrow> t" and Qg: "Q g"
shows "homotopic_with_canon Q U t f g"
proof -
have "continuous_on U (k \<circ> f)"
- using contf continuous_on_compose continuous_on_subset contk imf by blast
+ by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
moreover have "(k \<circ> f) ` U \<subseteq> S"
using imf imk by fastforce
moreover have "P (k \<circ> f)"
by (simp add: P Qf contf imf)
moreover have "continuous_on U (k \<circ> g)"
- using contg continuous_on_compose continuous_on_subset contk img by blast
+ by (meson contg continuous_on_compose continuous_on_subset contk funcset_image img)
moreover have "(k \<circ> g) ` U \<subseteq> S"
using img imk by fastforce
moreover have "P (k \<circ> g)"
by (simp add: P Qg contg img)
ultimately have "homotopic_with_canon P U S (k \<circ> f) (k \<circ> g)"
- by (rule hom)
+ by (simp add: hom image_subset_iff)
then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
using Q conth imh by force+
@@ -3228,23 +3228,23 @@
show "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
using Qeq topspace_euclidean_subtopology by blast
show "\<And>x. x \<in> U \<Longrightarrow> f x = h (k (f x))" "\<And>x. x \<in> U \<Longrightarrow> g x = h (k (g x))"
- using idhk imf img by auto
+ using idhk imf img by fastforce+
qed
qed
lemma homotopically_trivial_retraction_null_gen:
- assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
- and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+ assumes P: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+ and Q: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
- and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk>
+ and hom: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with_canon P U S f (\<lambda>x. c)"
- and contf: "continuous_on U f" and imf:"f ` U \<subseteq> t" and Qf: "Q f"
+ and contf: "continuous_on U f" and imf:"f \<in> U \<rightarrow> t" and Qf: "Q f"
obtains c where "homotopic_with_canon Q U t f (\<lambda>x. c)"
proof -
have feq: "\<And>x. x \<in> U \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
have "continuous_on U (k \<circ> f)"
- using contf continuous_on_compose continuous_on_subset contk imf by blast
- moreover have "(k \<circ> f) ` U \<subseteq> S"
+ by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
+ moreover have "(k \<circ> f) \<in> U \<rightarrow> S"
using imf imk by fastforce
moreover have "P (k \<circ> f)"
by (simp add: P Qf contf imf)
@@ -3265,32 +3265,32 @@
qed
lemma cohomotopically_trivial_retraction_gen:
- assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
- and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+ assumes P: "\<And>f. \<lbrakk>continuous_on t f; f \<in> t \<rightarrow> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+ and Q: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
- and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f;
- continuous_on S g; g ` S \<subseteq> U; P g\<rbrakk>
+ and hom: "\<And>f g. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f;
+ continuous_on S g; g \<in> S \<rightarrow> U; P g\<rbrakk>
\<Longrightarrow> homotopic_with_canon P S U f g"
- and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
- and contg: "continuous_on t g" and img: "g ` t \<subseteq> U" and Qg: "Q g"
+ and contf: "continuous_on t f" and imf: "f \<in> t \<rightarrow> U" and Qf: "Q f"
+ and contg: "continuous_on t g" and img: "g \<in> t \<rightarrow> U" and Qg: "Q g"
shows "homotopic_with_canon Q t U f g"
proof -
have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
have "continuous_on S (f \<circ> h)"
using contf conth continuous_on_compose imh by blast
- moreover have "(f \<circ> h) ` S \<subseteq> U"
+ moreover have "(f \<circ> h) \<in> S \<rightarrow> U"
using imf imh by fastforce
moreover have "P (f \<circ> h)"
by (simp add: P Qf contf imf)
moreover have "continuous_on S (g \<circ> h)"
using contg continuous_on_compose continuous_on_subset conth imh by blast
- moreover have "(g \<circ> h) ` S \<subseteq> U"
+ moreover have "(g \<circ> h) \<in> S \<rightarrow> U"
using img imh by fastforce
moreover have "P (g \<circ> h)"
by (simp add: P Qg contg img)
ultimately have "homotopic_with_canon P S U (f \<circ> h) (g \<circ> h)"
- by (rule hom)
+ by (simp add: hom)
then have "homotopic_with_canon Q t U (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q contk imk by force+
@@ -3303,18 +3303,18 @@
qed
lemma cohomotopically_trivial_retraction_null_gen:
- assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
- and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+ assumes P: "\<And>f. \<lbrakk>continuous_on t f; f \<in> t \<rightarrow> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+ and Q: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
- and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk>
+ and hom: "\<And>f g. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with_canon P S U f (\<lambda>x. c)"
- and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
+ and contf: "continuous_on t f" and imf: "f \<in> t \<rightarrow> U" and Qf: "Q f"
obtains c where "homotopic_with_canon Q t U f (\<lambda>x. c)"
proof -
have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
have "continuous_on S (f \<circ> h)"
using contf conth continuous_on_compose imh by blast
- moreover have "(f \<circ> h) ` S \<subseteq> U"
+ moreover have "(f \<circ> h) \<in> S \<rightarrow> U"
using imf imh by fastforce
moreover have "P (f \<circ> h)"
by (simp add: P Qf contf imf)
@@ -3335,12 +3335,12 @@
lemma simply_connected_retraction_gen:
shows "\<lbrakk>simply_connected S; continuous_on S h; h ` S = T;
- continuous_on T k; k ` T \<subseteq> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk>
+ continuous_on T k; k \<in> T \<rightarrow> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk>
\<Longrightarrow> simply_connected T"
apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify)
apply (rule Retracts.homotopically_trivial_retraction_gen
[of S h _ k _ "\<lambda>p. pathfinish p = pathstart p" "\<lambda>p. pathfinish p = pathstart p"])
-apply (simp_all add: Retracts_def pathfinish_def pathstart_def)
+apply (simp_all add: Retracts_def pathfinish_def pathstart_def image_subset_iff_funcset)
done
lemma homeomorphic_simply_connected: