4320 apply (rule homotopic_with_trans [OF _ hom]) |
4371 apply (rule homotopic_with_trans [OF _ hom]) |
4321 using homg apply (simp add: o_def) |
4372 using homg apply (simp add: o_def) |
4322 done |
4373 done |
4323 qed |
4374 qed |
4324 |
4375 |
|
4376 subsection\<open>Local versions of topological properties in general\<close> |
|
4377 |
|
4378 definition locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" |
|
4379 where |
|
4380 "locally P S \<equiv> |
|
4381 \<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w |
|
4382 \<longrightarrow> (\<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and> |
|
4383 x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)" |
|
4384 |
|
4385 lemma locallyI: |
|
4386 assumes "\<And>w x. \<lbrakk>openin (subtopology euclidean S) w; x \<in> w\<rbrakk> |
|
4387 \<Longrightarrow> \<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and> |
|
4388 x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w" |
|
4389 shows "locally P S" |
|
4390 using assms by (force simp: locally_def) |
|
4391 |
|
4392 lemma locallyE: |
|
4393 assumes "locally P S" "openin (subtopology euclidean S) w" "x \<in> w" |
|
4394 obtains u v where "openin (subtopology euclidean S) u" |
|
4395 "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> w" |
|
4396 using assms by (force simp: locally_def) |
|
4397 |
|
4398 lemma locally_mono: |
|
4399 assumes "locally P S" "\<And>t. P t \<Longrightarrow> Q t" |
|
4400 shows "locally Q S" |
|
4401 by (metis assms locally_def) |
|
4402 |
|
4403 lemma locally_open_subset: |
|
4404 assumes "locally P S" "openin (subtopology euclidean S) t" |
|
4405 shows "locally P t" |
|
4406 using assms |
|
4407 apply (simp add: locally_def) |
|
4408 apply (erule all_forward)+ |
|
4409 apply (rule impI) |
|
4410 apply (erule impCE) |
|
4411 using openin_trans apply blast |
|
4412 apply (erule ex_forward) |
|
4413 by (metis (no_types, hide_lams) Int_absorb1 Int_lower1 Int_subset_iff openin_open openin_subtopology_Int_subset) |
|
4414 |
|
4415 lemma locally_diff_closed: |
|
4416 "\<lbrakk>locally P S; closedin (subtopology euclidean S) t\<rbrakk> \<Longrightarrow> locally P (S - t)" |
|
4417 using locally_open_subset closedin_def by fastforce |
|
4418 |
|
4419 lemma locally_empty [iff]: "locally P {}" |
|
4420 by (simp add: locally_def openin_subtopology) |
|
4421 |
|
4422 lemma locally_singleton [iff]: |
|
4423 fixes a :: "'a::metric_space" |
|
4424 shows "locally P {a} \<longleftrightarrow> P {a}" |
|
4425 apply (simp add: locally_def openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR cong: conj_cong) |
|
4426 using zero_less_one by blast |
|
4427 |
|
4428 lemma locally_iff: |
|
4429 "locally P S \<longleftrightarrow> |
|
4430 (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>v. P v \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> v \<and> v \<subseteq> S \<inter> T)))" |
|
4431 apply (simp add: le_inf_iff locally_def openin_open, safe) |
|
4432 apply (metis IntE IntI le_inf_iff) |
|
4433 apply (metis IntI Int_subset_iff) |
|
4434 done |
|
4435 |
|
4436 lemma locally_Int: |
|
4437 assumes S: "locally P S" and t: "locally P t" |
|
4438 and P: "\<And>S t. P S \<and> P t \<Longrightarrow> P(S \<inter> t)" |
|
4439 shows "locally P (S \<inter> t)" |
|
4440 using S t unfolding locally_iff |
|
4441 apply clarify |
|
4442 apply (drule_tac x=T in spec)+ |
|
4443 apply (drule_tac x=x in spec)+ |
|
4444 apply clarsimp |
|
4445 apply (rename_tac U1 U2 V1 V2) |
|
4446 apply (rule_tac x="U1 \<inter> U2" in exI) |
|
4447 apply (simp add: open_Int) |
|
4448 apply (rule_tac x="V1 \<inter> V2" in exI) |
|
4449 apply (auto intro: P) |
|
4450 done |
|
4451 |
|
4452 |
|
4453 proposition homeomorphism_locally_imp: |
|
4454 fixes S :: "'a::metric_space set" and t :: "'b::t2_space set" |
|
4455 assumes S: "locally P S" and hom: "homeomorphism S t f g" |
|
4456 and Q: "\<And>S t. \<lbrakk>P S; homeomorphism S t f g\<rbrakk> \<Longrightarrow> Q t" |
|
4457 shows "locally Q t" |
|
4458 proof (clarsimp simp: locally_def) |
|
4459 fix w y |
|
4460 assume "y \<in> w" and "openin (subtopology euclidean t) w" |
|
4461 then obtain T where T: "open T" "w = t \<inter> T" |
|
4462 by (force simp: openin_open) |
|
4463 then have "w \<subseteq> t" by auto |
|
4464 have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f" |
|
4465 and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g" |
|
4466 using hom by (auto simp: homeomorphism_def) |
|
4467 have gw: "g ` w = S \<inter> {x. f x \<in> w}" |
|
4468 using \<open>w \<subseteq> t\<close> |
|
4469 apply auto |
|
4470 using \<open>g ` t = S\<close> \<open>w \<subseteq> t\<close> apply blast |
|
4471 using g \<open>w \<subseteq> t\<close> apply auto[1] |
|
4472 by (simp add: f rev_image_eqI) |
|
4473 have o: "openin (subtopology euclidean S) (g ` w)" |
|
4474 proof - |
|
4475 have "continuous_on S f" |
|
4476 using f(3) by blast |
|
4477 then show "openin (subtopology euclidean S) (g ` w)" |
|
4478 by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) w\<close> continuous_on_open f(2)) |
|
4479 qed |
|
4480 then obtain u v |
|
4481 where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` w" |
|
4482 using S [unfolded locally_def, rule_format, of "g ` w" "g y"] \<open>y \<in> w\<close> by force |
|
4483 have "v \<subseteq> S" using uv by (simp add: gw) |
|
4484 have fv: "f ` v = t \<inter> {x. g x \<in> v}" |
|
4485 using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto |
|
4486 have "f ` v \<subseteq> w" |
|
4487 using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto |
|
4488 have contvf: "continuous_on v f" |
|
4489 using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast |
|
4490 have contvg: "continuous_on (f ` v) g" |
|
4491 using \<open>f ` v \<subseteq> w\<close> \<open>w \<subseteq> t\<close> continuous_on_subset g(3) by blast |
|
4492 have homv: "homeomorphism v (f ` v) f g" |
|
4493 using \<open>v \<subseteq> S\<close> \<open>w \<subseteq> t\<close> f |
|
4494 apply (simp add: homeomorphism_def contvf contvg, auto) |
|
4495 by (metis f(1) rev_image_eqI rev_subsetD) |
|
4496 have 1: "openin (subtopology euclidean t) {x \<in> t. g x \<in> u}" |
|
4497 apply (rule continuous_on_open [THEN iffD1, rule_format]) |
|
4498 apply (rule \<open>continuous_on t g\<close>) |
|
4499 using \<open>g ` t = S\<close> apply (simp add: osu) |
|
4500 done |
|
4501 have 2: "\<exists>v. Q v \<and> y \<in> {x \<in> t. g x \<in> u} \<and> {x \<in> t. g x \<in> u} \<subseteq> v \<and> v \<subseteq> w" |
|
4502 apply (rule_tac x="f ` v" in exI) |
|
4503 apply (intro conjI Q [OF \<open>P v\<close> homv]) |
|
4504 using \<open>w \<subseteq> t\<close> \<open>y \<in> w\<close> \<open>f ` v \<subseteq> w\<close> uv apply (auto simp: fv) |
|
4505 done |
|
4506 show "\<exists>u. openin (subtopology euclidean t) u \<and> |
|
4507 (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)" |
|
4508 by (meson 1 2) |
|
4509 qed |
|
4510 |
|
4511 lemma homeomorphism_locally: |
|
4512 fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space" |
|
4513 assumes hom: "homeomorphism S t f g" |
|
4514 and eq: "\<And>S t. homeomorphism S t f g \<Longrightarrow> (P S \<longleftrightarrow> Q t)" |
|
4515 shows "locally P S \<longleftrightarrow> locally Q t" |
|
4516 apply (rule iffI) |
|
4517 apply (erule homeomorphism_locally_imp [OF _ hom]) |
|
4518 apply (simp add: eq) |
|
4519 apply (erule homeomorphism_locally_imp) |
|
4520 using eq homeomorphism_sym homeomorphism_symD [OF hom] apply blast+ |
|
4521 done |
|
4522 |
|
4523 lemma locally_translation: |
|
4524 fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool" |
|
4525 shows |
|
4526 "(\<And>S. P (image (\<lambda>x. a + x) S) \<longleftrightarrow> P S) |
|
4527 \<Longrightarrow> locally P (image (\<lambda>x. a + x) S) \<longleftrightarrow> locally P S" |
|
4528 apply (rule homeomorphism_locally [OF homeomorphism_translation]) |
|
4529 apply (simp add: homeomorphism_def) |
|
4530 by metis |
|
4531 |
|
4532 lemma locally_injective_linear_image: |
|
4533 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
4534 assumes f: "linear f" "inj f" and iff: "\<And>S. P (f ` S) \<longleftrightarrow> Q S" |
|
4535 shows "locally P (f ` S) \<longleftrightarrow> locally Q S" |
|
4536 apply (rule linear_homeomorphism_image [OF f]) |
|
4537 apply (rule_tac f=g and g = f in homeomorphism_locally, assumption) |
|
4538 by (metis iff homeomorphism_def) |
|
4539 |
|
4540 lemma locally_open_map_image: |
|
4541 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
|
4542 assumes P: "locally P S" |
|
4543 and f: "continuous_on S f" |
|
4544 and oo: "\<And>t. openin (subtopology euclidean S) t |
|
4545 \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` t)" |
|
4546 and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)" |
|
4547 shows "locally Q (f ` S)" |
|
4548 proof (clarsimp simp add: locally_def) |
|
4549 fix w y |
|
4550 assume oiw: "openin (subtopology euclidean (f ` S)) w" and "y \<in> w" |
|
4551 then have "w \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff) |
|
4552 have oivf: "openin (subtopology euclidean S) {x \<in> S. f x \<in> w}" |
|
4553 by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw]) |
|
4554 then obtain x where "x \<in> S" "f x = y" |
|
4555 using \<open>w \<subseteq> f ` S\<close> \<open>y \<in> w\<close> by blast |
|
4556 then obtain u v |
|
4557 where "openin (subtopology euclidean S) u" "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> {x \<in> S. f x \<in> w}" |
|
4558 using P [unfolded locally_def, rule_format, of "{x. x \<in> S \<and> f x \<in> w}" x] oivf \<open>y \<in> w\<close> |
|
4559 by auto |
|
4560 then show "\<exists>u. openin (subtopology euclidean (f ` S)) u \<and> |
|
4561 (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)" |
|
4562 apply (rule_tac x="f ` u" in exI) |
|
4563 apply (rule conjI, blast intro!: oo) |
|
4564 apply (rule_tac x="f ` v" in exI) |
|
4565 apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q) |
|
4566 done |
|
4567 qed |
|
4568 |
|
4569 subsection\<open>Basic properties of local compactness\<close> |
|
4570 |
|
4571 lemma locally_compact: |
|
4572 fixes s :: "'a :: metric_space set" |
|
4573 shows |
|
4574 "locally compact s \<longleftrightarrow> |
|
4575 (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> |
|
4576 openin (subtopology euclidean s) u \<and> compact v)" |
|
4577 (is "?lhs = ?rhs") |
|
4578 proof |
|
4579 assume ?lhs |
|
4580 then show ?rhs |
|
4581 apply clarify |
|
4582 apply (erule_tac w = "s \<inter> ball x 1" in locallyE) |
|
4583 by auto |
|
4584 next |
|
4585 assume r [rule_format]: ?rhs |
|
4586 have *: "\<exists>u v. |
|
4587 openin (subtopology euclidean s) u \<and> |
|
4588 compact v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<inter> T" |
|
4589 if "open T" "x \<in> s" "x \<in> T" for x T |
|
4590 proof - |
|
4591 obtain u v where uv: "x \<in> u" "u \<subseteq> v" "v \<subseteq> s" "compact v" "openin (subtopology euclidean s) u" |
|
4592 using r [OF \<open>x \<in> s\<close>] by auto |
|
4593 obtain e where "e>0" and e: "cball x e \<subseteq> T" |
|
4594 using open_contains_cball \<open>open T\<close> \<open>x \<in> T\<close> by blast |
|
4595 show ?thesis |
|
4596 apply (rule_tac x="(s \<inter> ball x e) \<inter> u" in exI) |
|
4597 apply (rule_tac x="cball x e \<inter> v" in exI) |
|
4598 using that \<open>e > 0\<close> e uv |
|
4599 apply auto |
|
4600 done |
|
4601 qed |
|
4602 show ?lhs |
|
4603 apply (rule locallyI) |
|
4604 apply (subst (asm) openin_open) |
|
4605 apply (blast intro: *) |
|
4606 done |
|
4607 qed |
|
4608 |
|
4609 lemma locally_compactE: |
|
4610 fixes s :: "'a :: metric_space set" |
|
4611 assumes "locally compact s" |
|
4612 obtains u v where "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and> |
|
4613 openin (subtopology euclidean s) (u x) \<and> compact (v x)" |
|
4614 using assms |
|
4615 unfolding locally_compact by metis |
|
4616 |
|
4617 lemma locally_compact_alt: |
|
4618 fixes s :: "'a :: heine_borel set" |
|
4619 shows "locally compact s \<longleftrightarrow> |
|
4620 (\<forall>x \<in> s. \<exists>u. x \<in> u \<and> |
|
4621 openin (subtopology euclidean s) u \<and> compact(closure u) \<and> closure u \<subseteq> s)" |
|
4622 apply (simp add: locally_compact) |
|
4623 apply (intro ball_cong ex_cong refl iffI) |
|
4624 apply (metis bounded_subset closure_eq closure_mono compact_eq_bounded_closed dual_order.trans) |
|
4625 by (meson closure_subset compact_closure) |
|
4626 |
|
4627 lemma locally_compact_Int_cball: |
|
4628 fixes s :: "'a :: heine_borel set" |
|
4629 shows "locally compact s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> closed(cball x e \<inter> s))" |
|
4630 (is "?lhs = ?rhs") |
|
4631 proof |
|
4632 assume ?lhs |
|
4633 then show ?rhs |
|
4634 apply (simp add: locally_compact openin_contains_cball) |
|
4635 apply (clarify | assumption | drule bspec)+ |
|
4636 by (metis (no_types, lifting) compact_cball compact_imp_closed compact_Int inf.absorb_iff2 inf.orderE inf_sup_aci(2)) |
|
4637 next |
|
4638 assume ?rhs |
|
4639 then show ?lhs |
|
4640 apply (simp add: locally_compact openin_contains_cball) |
|
4641 apply (clarify | assumption | drule bspec)+ |
|
4642 apply (rule_tac x="ball x e \<inter> s" in exI, simp) |
|
4643 apply (rule_tac x="cball x e \<inter> s" in exI) |
|
4644 using compact_eq_bounded_closed |
|
4645 apply auto |
|
4646 apply (metis open_ball le_infI1 mem_ball open_contains_cball_eq) |
|
4647 done |
|
4648 qed |
|
4649 |
|
4650 lemma locally_compact_compact: |
|
4651 fixes s :: "'a :: heine_borel set" |
|
4652 shows "locally compact s \<longleftrightarrow> |
|
4653 (\<forall>k. k \<subseteq> s \<and> compact k |
|
4654 \<longrightarrow> (\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> |
|
4655 openin (subtopology euclidean s) u \<and> compact v))" |
|
4656 (is "?lhs = ?rhs") |
|
4657 proof |
|
4658 assume ?lhs |
|
4659 then obtain u v where |
|
4660 uv: "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and> |
|
4661 openin (subtopology euclidean s) (u x) \<and> compact (v x)" |
|
4662 by (metis locally_compactE) |
|
4663 have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v" |
|
4664 if "k \<subseteq> s" "compact k" for k |
|
4665 proof - |
|
4666 have "\<And>C. (\<forall>c\<in>C. openin (subtopology euclidean k) c) \<and> k \<subseteq> \<Union>C \<Longrightarrow> |
|
4667 \<exists>D\<subseteq>C. finite D \<and> k \<subseteq> \<Union>D" |
|
4668 using that by (simp add: compact_eq_openin_cover) |
|
4669 moreover have "\<forall>c \<in> (\<lambda>x. k \<inter> u x) ` k. openin (subtopology euclidean k) c" |
|
4670 using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv) |
|
4671 moreover have "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` k)" |
|
4672 using that by clarsimp (meson subsetCE uv) |
|
4673 ultimately obtain D where "D \<subseteq> (\<lambda>x. k \<inter> u x) ` k" "finite D" "k \<subseteq> \<Union>D" |
|
4674 by metis |
|
4675 then obtain T where T: "T \<subseteq> k" "finite T" "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` T)" |
|
4676 by (metis finite_subset_image) |
|
4677 have Tuv: "UNION T u \<subseteq> UNION T v" |
|
4678 using T that by (force simp: dest!: uv) |
|
4679 show ?thesis |
|
4680 apply (rule_tac x="\<Union>(u ` T)" in exI) |
|
4681 apply (rule_tac x="\<Union>(v ` T)" in exI) |
|
4682 apply (simp add: Tuv) |
|
4683 using T that |
|
4684 apply (auto simp: dest!: uv) |
|
4685 done |
|
4686 qed |
|
4687 show ?rhs |
|
4688 by (blast intro: *) |
|
4689 next |
|
4690 assume ?rhs |
|
4691 then show ?lhs |
|
4692 apply (clarsimp simp add: locally_compact) |
|
4693 apply (drule_tac x="{x}" in spec, simp) |
|
4694 done |
|
4695 qed |
|
4696 |
|
4697 lemma open_imp_locally_compact: |
|
4698 fixes s :: "'a :: heine_borel set" |
|
4699 assumes "open s" |
|
4700 shows "locally compact s" |
|
4701 proof - |
|
4702 have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v" |
|
4703 if "x \<in> s" for x |
|
4704 proof - |
|
4705 obtain e where "e>0" and e: "cball x e \<subseteq> s" |
|
4706 using open_contains_cball assms \<open>x \<in> s\<close> by blast |
|
4707 have ope: "openin (subtopology euclidean s) (ball x e)" |
|
4708 by (meson e open_ball ball_subset_cball dual_order.trans open_subset) |
|
4709 show ?thesis |
|
4710 apply (rule_tac x="ball x e" in exI) |
|
4711 apply (rule_tac x="cball x e" in exI) |
|
4712 using \<open>e > 0\<close> e apply (auto simp: ope) |
|
4713 done |
|
4714 qed |
|
4715 show ?thesis |
|
4716 unfolding locally_compact |
|
4717 by (blast intro: *) |
|
4718 qed |
|
4719 |
|
4720 lemma closed_imp_locally_compact: |
|
4721 fixes s :: "'a :: heine_borel set" |
|
4722 assumes "closed s" |
|
4723 shows "locally compact s" |
|
4724 proof - |
|
4725 have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> |
|
4726 openin (subtopology euclidean s) u \<and> compact v" |
|
4727 if "x \<in> s" for x |
|
4728 proof - |
|
4729 show ?thesis |
|
4730 apply (rule_tac x = "s \<inter> ball x 1" in exI) |
|
4731 apply (rule_tac x = "s \<inter> cball x 1" in exI) |
|
4732 using \<open>x \<in> s\<close> assms apply auto |
|
4733 done |
|
4734 qed |
|
4735 show ?thesis |
|
4736 unfolding locally_compact |
|
4737 by (blast intro: *) |
|
4738 qed |
|
4739 |
|
4740 lemma locally_compact_UNIV: "locally compact (UNIV :: 'a :: heine_borel set)" |
|
4741 by (simp add: closed_imp_locally_compact) |
|
4742 |
|
4743 lemma locally_compact_Int: |
|
4744 fixes s :: "'a :: t2_space set" |
|
4745 shows "\<lbrakk>locally compact s; locally compact t\<rbrakk> \<Longrightarrow> locally compact (s \<inter> t)" |
|
4746 by (simp add: compact_Int locally_Int) |
|
4747 |
|
4748 lemma locally_compact_closedin: |
|
4749 fixes s :: "'a :: heine_borel set" |
|
4750 shows "\<lbrakk>closedin (subtopology euclidean s) t; locally compact s\<rbrakk> |
|
4751 \<Longrightarrow> locally compact t" |
|
4752 unfolding closedin_closed |
|
4753 using closed_imp_locally_compact locally_compact_Int by blast |
|
4754 |
|
4755 lemma locally_compact_delete: |
|
4756 fixes s :: "'a :: t1_space set" |
|
4757 shows "locally compact s \<Longrightarrow> locally compact (s - {a})" |
|
4758 by (auto simp: openin_delete locally_open_subset) |
|
4759 |
|
4760 lemma locally_closed: |
|
4761 fixes s :: "'a :: heine_borel set" |
|
4762 shows "locally closed s \<longleftrightarrow> locally compact s" |
|
4763 (is "?lhs = ?rhs") |
|
4764 proof |
|
4765 assume ?lhs |
|
4766 then show ?rhs |
|
4767 apply (simp only: locally_def) |
|
4768 apply (erule all_forward imp_forward asm_rl exE)+ |
|
4769 apply (rule_tac x = "u \<inter> ball x 1" in exI) |
|
4770 apply (rule_tac x = "v \<inter> cball x 1" in exI) |
|
4771 apply (force intro: openin_trans) |
|
4772 done |
|
4773 next |
|
4774 assume ?rhs then show ?lhs |
|
4775 using compact_eq_bounded_closed locally_mono by blast |
|
4776 qed |
|
4777 |
|
4778 subsection\<open>Important special cases of local connectedness and path connectedness\<close> |
|
4779 |
|
4780 lemma locally_connected_1: |
|
4781 assumes |
|
4782 "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk> |
|
4783 \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and> |
|
4784 connected u \<and> x \<in> u \<and> u \<subseteq> v" |
|
4785 shows "locally connected S" |
|
4786 apply (clarsimp simp add: locally_def) |
|
4787 apply (drule assms; blast) |
|
4788 done |
|
4789 |
|
4790 lemma locally_connected_2: |
|
4791 assumes "locally connected S" |
|
4792 "openin (subtopology euclidean S) t" |
|
4793 "x \<in> t" |
|
4794 shows "openin (subtopology euclidean S) (connected_component_set t x)" |
|
4795 proof - |
|
4796 { fix y :: 'a |
|
4797 let ?SS = "subtopology euclidean S" |
|
4798 assume 1: "openin ?SS t" |
|
4799 "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))" |
|
4800 and "connected_component t x y" |
|
4801 then have "y \<in> t" and y: "y \<in> connected_component_set t x" |
|
4802 using connected_component_subset by blast+ |
|
4803 obtain F where |
|
4804 "\<forall>x y. (\<exists>w. openin ?SS w \<and> (\<exists>u. connected u \<and> x \<in> w \<and> w \<subseteq> u \<and> u \<subseteq> y)) = (openin ?SS (F x y) \<and> (\<exists>u. connected u \<and> x \<in> F x y \<and> F x y \<subseteq> u \<and> u \<subseteq> y))" |
|
4805 by moura |
|
4806 then obtain G where |
|
4807 "\<forall>a A. (\<exists>U. openin ?SS U \<and> (\<exists>V. connected V \<and> a \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> A)) = (openin ?SS (F a A) \<and> connected (G a A) \<and> a \<in> F a A \<and> F a A \<subseteq> G a A \<and> G a A \<subseteq> A)" |
|
4808 by moura |
|
4809 then have *: "openin ?SS (F y t) \<and> connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t" |
|
4810 using 1 \<open>y \<in> t\<close> by presburger |
|
4811 have "G y t \<subseteq> connected_component_set t y" |
|
4812 by (metis (no_types) * connected_component_eq_self connected_component_mono contra_subsetD) |
|
4813 then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> connected_component_set t x" |
|
4814 by (metis (no_types) * connected_component_eq dual_order.trans y) |
|
4815 } |
|
4816 then show ?thesis |
|
4817 using assms openin_subopen by (force simp: locally_def) |
|
4818 qed |
|
4819 |
|
4820 lemma locally_connected_3: |
|
4821 assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk> |
|
4822 \<Longrightarrow> openin (subtopology euclidean S) |
|
4823 (connected_component_set t x)" |
|
4824 "openin (subtopology euclidean S) v" "x \<in> v" |
|
4825 shows "\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v" |
|
4826 using assms connected_component_subset by fastforce |
|
4827 |
|
4828 lemma locally_connected: |
|
4829 "locally connected S \<longleftrightarrow> |
|
4830 (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v |
|
4831 \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v))" |
|
4832 by (metis locally_connected_1 locally_connected_2 locally_connected_3) |
|
4833 |
|
4834 lemma locally_connected_open_connected_component: |
|
4835 "locally connected S \<longleftrightarrow> |
|
4836 (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t |
|
4837 \<longrightarrow> openin (subtopology euclidean S) (connected_component_set t x))" |
|
4838 by (metis locally_connected_1 locally_connected_2 locally_connected_3) |
|
4839 |
|
4840 lemma locally_path_connected_1: |
|
4841 assumes |
|
4842 "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk> |
|
4843 \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v" |
|
4844 shows "locally path_connected S" |
|
4845 apply (clarsimp simp add: locally_def) |
|
4846 apply (drule assms; blast) |
|
4847 done |
|
4848 |
|
4849 lemma locally_path_connected_2: |
|
4850 assumes "locally path_connected S" |
|
4851 "openin (subtopology euclidean S) t" |
|
4852 "x \<in> t" |
|
4853 shows "openin (subtopology euclidean S) (path_component_set t x)" |
|
4854 proof - |
|
4855 { fix y :: 'a |
|
4856 let ?SS = "subtopology euclidean S" |
|
4857 assume 1: "openin ?SS t" |
|
4858 "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. path_connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))" |
|
4859 and "path_component t x y" |
|
4860 then have "y \<in> t" and y: "y \<in> path_component_set t x" |
|
4861 using path_component_mem(2) by blast+ |
|
4862 obtain F where |
|
4863 "\<forall>x y. (\<exists>w. openin ?SS w \<and> (\<exists>u. path_connected u \<and> x \<in> w \<and> w \<subseteq> u \<and> u \<subseteq> y)) = (openin ?SS (F x y) \<and> (\<exists>u. path_connected u \<and> x \<in> F x y \<and> F x y \<subseteq> u \<and> u \<subseteq> y))" |
|
4864 by moura |
|
4865 then obtain G where |
|
4866 "\<forall>a A. (\<exists>U. openin ?SS U \<and> (\<exists>V. path_connected V \<and> a \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> A)) = (openin ?SS (F a A) \<and> path_connected (G a A) \<and> a \<in> F a A \<and> F a A \<subseteq> G a A \<and> G a A \<subseteq> A)" |
|
4867 by moura |
|
4868 then have *: "openin ?SS (F y t) \<and> path_connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t" |
|
4869 using 1 \<open>y \<in> t\<close> by presburger |
|
4870 have "G y t \<subseteq> path_component_set t y" |
|
4871 using * path_component_maximal set_rev_mp by blast |
|
4872 then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x" |
|
4873 by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y) |
|
4874 } |
|
4875 then show ?thesis |
|
4876 using assms openin_subopen by (force simp: locally_def) |
|
4877 qed |
|
4878 |
|
4879 lemma locally_path_connected_3: |
|
4880 assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk> |
|
4881 \<Longrightarrow> openin (subtopology euclidean S) (path_component_set t x)" |
|
4882 "openin (subtopology euclidean S) v" "x \<in> v" |
|
4883 shows "\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v" |
|
4884 proof - |
|
4885 have "path_component v x x" |
|
4886 by (meson assms(3) path_component_refl) |
|
4887 then show ?thesis |
|
4888 by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component) |
|
4889 qed |
|
4890 |
|
4891 proposition locally_path_connected: |
|
4892 "locally path_connected S \<longleftrightarrow> |
|
4893 (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v |
|
4894 \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))" |
|
4895 by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) |
|
4896 |
|
4897 proposition locally_path_connected_open_path_connected_component: |
|
4898 "locally path_connected S \<longleftrightarrow> |
|
4899 (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t |
|
4900 \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))" |
|
4901 by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) |
|
4902 |
|
4903 lemma locally_connected_open_component: |
|
4904 "locally connected S \<longleftrightarrow> |
|
4905 (\<forall>t c. openin (subtopology euclidean S) t \<and> c \<in> components t |
|
4906 \<longrightarrow> openin (subtopology euclidean S) c)" |
|
4907 by (metis components_iff locally_connected_open_connected_component) |
|
4908 |
|
4909 proposition locally_connected_im_kleinen: |
|
4910 "locally connected S \<longleftrightarrow> |
|
4911 (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v |
|
4912 \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> |
|
4913 x \<in> u \<and> u \<subseteq> v \<and> |
|
4914 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))" |
|
4915 (is "?lhs = ?rhs") |
|
4916 proof |
|
4917 assume ?lhs |
|
4918 then show ?rhs |
|
4919 by (fastforce simp add: locally_connected) |
|
4920 next |
|
4921 assume ?rhs |
|
4922 have *: "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> c" |
|
4923 if "openin (subtopology euclidean S) t" and c: "c \<in> components t" and "x \<in> c" for t c x |
|
4924 proof - |
|
4925 from that \<open>?rhs\<close> [rule_format, of t x] |
|
4926 obtain u where u: |
|
4927 "openin (subtopology euclidean S) u \<and> x \<in> u \<and> u \<subseteq> t \<and> |
|
4928 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> t \<and> x \<in> c \<and> y \<in> c))" |
|
4929 by auto (meson subsetD in_components_subset) |
|
4930 obtain F :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where |
|
4931 "\<forall>x y. (\<exists>z. z \<in> x \<and> y = connected_component_set x z) = (F x y \<in> x \<and> y = connected_component_set x (F x y))" |
|
4932 by moura |
|
4933 then have F: "F t c \<in> t \<and> c = connected_component_set t (F t c)" |
|
4934 by (meson components_iff c) |
|
4935 obtain G :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where |
|
4936 G: "\<forall>x y. (\<exists>z. z \<in> y \<and> z \<notin> x) = (G x y \<in> y \<and> G x y \<notin> x)" |
|
4937 by moura |
|
4938 have "G c u \<notin> u \<or> G c u \<in> c" |
|
4939 using F by (metis (full_types) u connected_componentI connected_component_eq mem_Collect_eq that(3)) |
|
4940 then show ?thesis |
|
4941 using G u by auto |
|
4942 qed |
|
4943 show ?lhs |
|
4944 apply (clarsimp simp add: locally_connected_open_component) |
|
4945 apply (subst openin_subopen) |
|
4946 apply (blast intro: *) |
|
4947 done |
|
4948 qed |
|
4949 |
|
4950 proposition locally_path_connected_im_kleinen: |
|
4951 "locally path_connected S \<longleftrightarrow> |
|
4952 (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v |
|
4953 \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> |
|
4954 x \<in> u \<and> u \<subseteq> v \<and> |
|
4955 (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and> |
|
4956 pathstart p = x \<and> pathfinish p = y))))" |
|
4957 (is "?lhs = ?rhs") |
|
4958 proof |
|
4959 assume ?lhs |
|
4960 then show ?rhs |
|
4961 apply (simp add: locally_path_connected path_connected_def) |
|
4962 apply (erule all_forward ex_forward imp_forward conjE | simp)+ |
|
4963 by (meson dual_order.trans) |
|
4964 next |
|
4965 assume ?rhs |
|
4966 have *: "\<exists>T. openin (subtopology euclidean S) T \<and> |
|
4967 x \<in> T \<and> T \<subseteq> path_component_set u z" |
|
4968 if "openin (subtopology euclidean S) u" and "z \<in> u" and c: "path_component u z x" for u z x |
|
4969 proof - |
|
4970 have "x \<in> u" |
|
4971 by (meson c path_component_mem(2)) |
|
4972 with that \<open>?rhs\<close> [rule_format, of u x] |
|
4973 obtain U where U: |
|
4974 "openin (subtopology euclidean S) U \<and> x \<in> U \<and> U \<subseteq> u \<and> |
|
4975 (\<forall>y. y \<in> U \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> u \<and> pathstart p = x \<and> pathfinish p = y))" |
|
4976 by blast |
|
4977 show ?thesis |
|
4978 apply (rule_tac x=U in exI) |
|
4979 apply (auto simp: U) |
|
4980 apply (metis U c path_component_trans path_component_def) |
|
4981 done |
|
4982 qed |
|
4983 show ?lhs |
|
4984 apply (clarsimp simp add: locally_path_connected_open_path_connected_component) |
|
4985 apply (subst openin_subopen) |
|
4986 apply (blast intro: *) |
|
4987 done |
|
4988 qed |
|
4989 |
|
4990 lemma locally_path_connected_imp_locally_connected: |
|
4991 "locally path_connected S \<Longrightarrow> locally connected S" |
|
4992 using locally_mono path_connected_imp_connected by blast |
|
4993 |
|
4994 lemma locally_connected_components: |
|
4995 "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> locally connected c" |
|
4996 by (meson locally_connected_open_component locally_open_subset openin_subtopology_self) |
|
4997 |
|
4998 lemma locally_path_connected_components: |
|
4999 "\<lbrakk>locally path_connected S; c \<in> components S\<rbrakk> \<Longrightarrow> locally path_connected c" |
|
5000 by (meson locally_connected_open_component locally_open_subset locally_path_connected_imp_locally_connected openin_subtopology_self) |
|
5001 |
|
5002 lemma locally_path_connected_connected_component: |
|
5003 "locally path_connected S \<Longrightarrow> locally path_connected (connected_component_set S x)" |
|
5004 by (metis components_iff connected_component_eq_empty locally_empty locally_path_connected_components) |
|
5005 |
|
5006 lemma open_imp_locally_path_connected: |
|
5007 fixes S :: "'a :: real_normed_vector set" |
|
5008 shows "open S \<Longrightarrow> locally path_connected S" |
|
5009 apply (rule locally_mono [of convex]) |
|
5010 apply (simp_all add: locally_def openin_open_eq convex_imp_path_connected) |
|
5011 apply (meson Topology_Euclidean_Space.open_ball centre_in_ball convex_ball openE order_trans) |
|
5012 done |
|
5013 |
|
5014 lemma open_imp_locally_connected: |
|
5015 fixes S :: "'a :: real_normed_vector set" |
|
5016 shows "open S \<Longrightarrow> locally connected S" |
|
5017 by (simp add: locally_path_connected_imp_locally_connected open_imp_locally_path_connected) |
|
5018 |
|
5019 lemma locally_path_connected_UNIV: "locally path_connected (UNIV::'a :: real_normed_vector set)" |
|
5020 by (simp add: open_imp_locally_path_connected) |
|
5021 |
|
5022 lemma locally_connected_UNIV: "locally connected (UNIV::'a :: real_normed_vector set)" |
|
5023 by (simp add: open_imp_locally_connected) |
|
5024 |
|
5025 lemma openin_connected_component_locally_connected: |
|
5026 "locally connected S |
|
5027 \<Longrightarrow> openin (subtopology euclidean S) (connected_component_set S x)" |
|
5028 apply (simp add: locally_connected_open_connected_component) |
|
5029 by (metis connected_component_eq_empty connected_component_subset open_empty open_subset openin_subtopology_self) |
|
5030 |
|
5031 lemma openin_components_locally_connected: |
|
5032 "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) c" |
|
5033 using locally_connected_open_component openin_subtopology_self by blast |
|
5034 |
|
5035 lemma openin_path_component_locally_path_connected: |
|
5036 "locally path_connected S |
|
5037 \<Longrightarrow> openin (subtopology euclidean S) (path_component_set S x)" |
|
5038 by (metis (no_types) empty_iff locally_path_connected_2 openin_subopen openin_subtopology_self path_component_eq_empty) |
|
5039 |
|
5040 lemma closedin_path_component_locally_path_connected: |
|
5041 "locally path_connected S |
|
5042 \<Longrightarrow> closedin (subtopology euclidean S) (path_component_set S x)" |
|
5043 apply (simp add: closedin_def path_component_subset complement_path_component_Union) |
|
5044 apply (rule openin_Union) |
|
5045 using openin_path_component_locally_path_connected by auto |
|
5046 |
|
5047 lemma convex_imp_locally_path_connected: |
|
5048 fixes S :: "'a:: real_normed_vector set" |
|
5049 shows "convex S \<Longrightarrow> locally path_connected S" |
|
5050 apply (clarsimp simp add: locally_path_connected) |
|
5051 apply (subst (asm) openin_open) |
|
5052 apply clarify |
|
5053 apply (erule (1) Topology_Euclidean_Space.openE) |
|
5054 apply (rule_tac x = "S \<inter> ball x e" in exI) |
|
5055 apply (force simp: convex_Int convex_imp_path_connected) |
|
5056 done |
|
5057 |
|
5058 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close> |
|
5059 |
|
5060 locale Retracts = |
|
5061 fixes s h t k |
|
5062 assumes conth: "continuous_on s h" |
|
5063 and imh: "h ` s = t" |
|
5064 and contk: "continuous_on t k" |
|
5065 and imk: "k ` t \<subseteq> s" |
|
5066 and idhk: "\<And>y. y \<in> t \<Longrightarrow> h(k y) = y" |
|
5067 |
|
5068 begin |
|
5069 |
|
5070 lemma homotopically_trivial_retraction_gen: |
|
5071 assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)" |
|
5072 and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)" |
|
5073 and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k" |
|
5074 and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f; |
|
5075 continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk> |
|
5076 \<Longrightarrow> homotopic_with P u s f g" |
|
5077 and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f" |
|
5078 and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g" |
|
5079 shows "homotopic_with Q u t f g" |
|
5080 proof - |
|
5081 have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto |
|
5082 have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto |
|
5083 have "continuous_on u (k \<circ> f)" |
|
5084 using contf continuous_on_compose continuous_on_subset contk imf by blast |
|
5085 moreover have "(k \<circ> f) ` u \<subseteq> s" |
|
5086 using imf imk by fastforce |
|
5087 moreover have "P (k \<circ> f)" |
|
5088 by (simp add: P Qf contf imf) |
|
5089 moreover have "continuous_on u (k \<circ> g)" |
|
5090 using contg continuous_on_compose continuous_on_subset contk img by blast |
|
5091 moreover have "(k \<circ> g) ` u \<subseteq> s" |
|
5092 using img imk by fastforce |
|
5093 moreover have "P (k \<circ> g)" |
|
5094 by (simp add: P Qg contg img) |
|
5095 ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)" |
|
5096 by (rule hom) |
|
5097 then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))" |
|
5098 apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) |
|
5099 using Q by (auto simp: conth imh) |
|
5100 then show ?thesis |
|
5101 apply (rule homotopic_with_eq) |
|
5102 apply (metis feq) |
|
5103 apply (metis geq) |
|
5104 apply (metis Qeq) |
|
5105 done |
|
5106 qed |
|
5107 |
|
5108 lemma homotopically_trivial_retraction_null_gen: |
|
5109 assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)" |
|
5110 and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)" |
|
5111 and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k" |
|
5112 and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> |
|
5113 \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)" |
|
5114 and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f" |
|
5115 obtains c where "homotopic_with Q u t f (\<lambda>x. c)" |
|
5116 proof - |
|
5117 have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto |
|
5118 have "continuous_on u (k \<circ> f)" |
|
5119 using contf continuous_on_compose continuous_on_subset contk imf by blast |
|
5120 moreover have "(k \<circ> f) ` u \<subseteq> s" |
|
5121 using imf imk by fastforce |
|
5122 moreover have "P (k \<circ> f)" |
|
5123 by (simp add: P Qf contf imf) |
|
5124 ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)" |
|
5125 by (metis hom) |
|
5126 then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h o (\<lambda>x. c))" |
|
5127 apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) |
|
5128 using Q by (auto simp: conth imh) |
|
5129 then show ?thesis |
|
5130 apply (rule_tac c = "h c" in that) |
|
5131 apply (erule homotopic_with_eq) |
|
5132 apply (metis feq, simp) |
|
5133 apply (metis Qeq) |
|
5134 done |
|
5135 qed |
|
5136 |
|
5137 lemma cohomotopically_trivial_retraction_gen: |
|
5138 assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)" |
|
5139 and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)" |
|
5140 and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k" |
|
5141 and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f; |
|
5142 continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk> |
|
5143 \<Longrightarrow> homotopic_with P s u f g" |
|
5144 and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f" |
|
5145 and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g" |
|
5146 shows "homotopic_with Q t u f g" |
|
5147 proof - |
|
5148 have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto |
|
5149 have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto |
|
5150 have "continuous_on s (f \<circ> h)" |
|
5151 using contf conth continuous_on_compose imh by blast |
|
5152 moreover have "(f \<circ> h) ` s \<subseteq> u" |
|
5153 using imf imh by fastforce |
|
5154 moreover have "P (f \<circ> h)" |
|
5155 by (simp add: P Qf contf imf) |
|
5156 moreover have "continuous_on s (g o h)" |
|
5157 using contg continuous_on_compose continuous_on_subset conth imh by blast |
|
5158 moreover have "(g \<circ> h) ` s \<subseteq> u" |
|
5159 using img imh by fastforce |
|
5160 moreover have "P (g \<circ> h)" |
|
5161 by (simp add: P Qg contg img) |
|
5162 ultimately have "homotopic_with P s u (f o h) (g \<circ> h)" |
|
5163 by (rule hom) |
|
5164 then have "homotopic_with Q t u (f o h o k) (g \<circ> h o k)" |
|
5165 apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) |
|
5166 using Q by (auto simp: contk imk) |
|
5167 then show ?thesis |
|
5168 apply (rule homotopic_with_eq) |
|
5169 apply (metis feq) |
|
5170 apply (metis geq) |
|
5171 apply (metis Qeq) |
|
5172 done |
|
5173 qed |
|
5174 |
|
5175 lemma cohomotopically_trivial_retraction_null_gen: |
|
5176 assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)" |
|
5177 and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)" |
|
5178 and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k" |
|
5179 and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> |
|
5180 \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)" |
|
5181 and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f" |
|
5182 obtains c where "homotopic_with Q t u f (\<lambda>x. c)" |
|
5183 proof - |
|
5184 have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto |
|
5185 have "continuous_on s (f \<circ> h)" |
|
5186 using contf conth continuous_on_compose imh by blast |
|
5187 moreover have "(f \<circ> h) ` s \<subseteq> u" |
|
5188 using imf imh by fastforce |
|
5189 moreover have "P (f \<circ> h)" |
|
5190 by (simp add: P Qf contf imf) |
|
5191 ultimately obtain c where "homotopic_with P s u (f o h) (\<lambda>x. c)" |
|
5192 by (metis hom) |
|
5193 then have "homotopic_with Q t u (f o h o k) ((\<lambda>x. c) o k)" |
|
5194 apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) |
|
5195 using Q by (auto simp: contk imk) |
|
5196 then show ?thesis |
|
5197 apply (rule_tac c = c in that) |
|
5198 apply (erule homotopic_with_eq) |
|
5199 apply (metis feq, simp) |
|
5200 apply (metis Qeq) |
|
5201 done |
|
5202 qed |
|
5203 |
4325 end |
5204 end |
|
5205 |
|
5206 lemma simply_connected_retraction_gen: |
|
5207 shows "\<lbrakk>simply_connected S; continuous_on S h; h ` S = T; |
|
5208 continuous_on T k; k ` T \<subseteq> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk> |
|
5209 \<Longrightarrow> simply_connected T" |
|
5210 apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify) |
|
5211 apply (rule Retracts.homotopically_trivial_retraction_gen |
|
5212 [of S h _ k _ "\<lambda>p. pathfinish p = pathstart p" "\<lambda>p. pathfinish p = pathstart p"]) |
|
5213 apply (simp_all add: Retracts_def pathfinish_def pathstart_def) |
|
5214 done |
|
5215 |
|
5216 lemma homeomorphic_simply_connected: |
|
5217 "\<lbrakk>S homeomorphic T; simply_connected S\<rbrakk> \<Longrightarrow> simply_connected T" |
|
5218 by (auto simp: homeomorphic_def homeomorphism_def intro: simply_connected_retraction_gen) |
|
5219 |
|
5220 lemma homeomorphic_simply_connected_eq: |
|
5221 "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)" |
|
5222 by (metis homeomorphic_simply_connected homeomorphic_sym) |
|
5223 |
|
5224 end |