3554 by (metis continuous_on_eq_continuous_within open_vimage) |
3554 by (metis continuous_on_eq_continuous_within open_vimage) |
3555 |
3555 |
3556 lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)" |
3556 lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)" |
3557 by (simp add: closed_vimage continuous_on_eq_continuous_within) |
3557 by (simp add: closed_vimage continuous_on_eq_continuous_within) |
3558 |
3558 |
|
3559 lemma Times_in_interior_subtopology: |
|
3560 assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U" |
|
3561 obtains V W where "openin (subtopology euclidean S) V" "x \<in> V" |
|
3562 "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U" |
|
3563 proof - |
|
3564 from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T" |
|
3565 by (auto simp: openin_open) |
|
3566 from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>] |
|
3567 obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E" |
|
3568 by blast |
|
3569 show ?thesis |
|
3570 proof |
|
3571 show "openin (subtopology euclidean S) (E1 \<inter> S)" |
|
3572 "openin (subtopology euclidean T) (E2 \<inter> T)" |
|
3573 using \<open>open E1\<close> \<open>open E2\<close> |
|
3574 by (auto simp: openin_open) |
|
3575 show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T" |
|
3576 using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto |
|
3577 show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U" |
|
3578 using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close> |
|
3579 by (auto simp: ) |
|
3580 qed |
|
3581 qed |
|
3582 |
|
3583 lemma closedin_Times: |
|
3584 "closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow> |
|
3585 closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')" |
|
3586 unfolding closedin_closed using closed_Times by blast |
|
3587 |
|
3588 lemma openin_Times: |
|
3589 "openin (subtopology euclidean S) S' \<Longrightarrow> openin (subtopology euclidean T) T' \<Longrightarrow> |
|
3590 openin (subtopology euclidean (S \<times> T)) (S' \<times> T')" |
|
3591 unfolding openin_open using open_Times by blast |
|
3592 |
|
3593 lemma openin_Times_eq: |
|
3594 fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" |
|
3595 shows |
|
3596 "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow> |
|
3597 S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'" |
|
3598 (is "?lhs = ?rhs") |
|
3599 proof (cases "S' = {} \<or> T' = {}") |
|
3600 case True |
|
3601 then show ?thesis by auto |
|
3602 next |
|
3603 case False |
|
3604 then obtain x y where "x \<in> S'" "y \<in> T'" |
|
3605 by blast |
|
3606 show ?thesis |
|
3607 proof |
|
3608 assume ?lhs |
|
3609 have "openin (subtopology euclidean S) S'" |
|
3610 apply (subst openin_subopen, clarify) |
|
3611 apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>]) |
|
3612 using \<open>y \<in> T'\<close> |
|
3613 apply auto |
|
3614 done |
|
3615 moreover have "openin (subtopology euclidean T) T'" |
|
3616 apply (subst openin_subopen, clarify) |
|
3617 apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>]) |
|
3618 using \<open>x \<in> S'\<close> |
|
3619 apply auto |
|
3620 done |
|
3621 ultimately show ?rhs |
|
3622 by simp |
|
3623 next |
|
3624 assume ?rhs |
|
3625 with False show ?lhs |
|
3626 by (simp add: openin_Times) |
|
3627 qed |
|
3628 qed |
|
3629 |
|
3630 lemma Lim_transform_within_openin: |
|
3631 assumes f: "(f \<longlongrightarrow> l) (at a within T)" |
|
3632 and "openin (subtopology euclidean T) S" "a \<in> S" |
|
3633 and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x" |
|
3634 shows "(g \<longlongrightarrow> l) (at a within T)" |
|
3635 proof - |
|
3636 have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a" |
|
3637 by (simp add: eventually_at_filter) |
|
3638 moreover |
|
3639 from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U" |
|
3640 by (auto simp: openin_open) |
|
3641 then have "a \<in> U" using \<open>a \<in> S\<close> by auto |
|
3642 from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>] |
|
3643 have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto |
|
3644 ultimately |
|
3645 have "\<forall>\<^sub>F x in at a within T. f x = g x" |
|
3646 by eventually_elim (auto simp: \<open>S = _\<close> eq) |
|
3647 then show ?thesis using f |
|
3648 by (rule Lim_transform_eventually) |
|
3649 qed |
|
3650 |
|
3651 lemma continuous_on_open_gen: |
|
3652 assumes "f ` S \<subseteq> T" |
|
3653 shows "continuous_on S f \<longleftrightarrow> |
|
3654 (\<forall>U. openin (subtopology euclidean T) U |
|
3655 \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))" |
|
3656 (is "?lhs = ?rhs") |
|
3657 proof |
|
3658 assume ?lhs |
|
3659 then show ?rhs |
|
3660 by (clarsimp simp add: continuous_openin_preimage_eq openin_open) |
|
3661 (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1) |
|
3662 next |
|
3663 assume R [rule_format]: ?rhs |
|
3664 show ?lhs |
|
3665 proof (clarsimp simp add: continuous_openin_preimage_eq) |
|
3666 fix U::"'a set" |
|
3667 assume "open U" |
|
3668 then have "openin (subtopology euclidean S) (S \<inter> f -` (U \<inter> T))" |
|
3669 by (metis R inf_commute openin_open) |
|
3670 then show "openin (subtopology euclidean S) (S \<inter> f -` U)" |
|
3671 by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int) |
|
3672 qed |
|
3673 qed |
|
3674 |
|
3675 lemma continuous_openin_preimage: |
|
3676 "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk> |
|
3677 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)" |
|
3678 by (simp add: continuous_on_open_gen) |
|
3679 |
|
3680 lemma continuous_on_closed_gen: |
|
3681 assumes "f ` S \<subseteq> T" |
|
3682 shows "continuous_on S f \<longleftrightarrow> |
|
3683 (\<forall>U. closedin (subtopology euclidean T) U |
|
3684 \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))" |
|
3685 (is "?lhs = ?rhs") |
|
3686 proof - |
|
3687 have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U |
|
3688 using assms by blast |
|
3689 show ?thesis |
|
3690 proof |
|
3691 assume L: ?lhs |
|
3692 show ?rhs |
|
3693 proof clarify |
|
3694 fix U |
|
3695 assume "closedin (subtopology euclidean T) U" |
|
3696 then show "closedin (subtopology euclidean S) (S \<inter> f -` U)" |
|
3697 using L unfolding continuous_on_open_gen [OF assms] |
|
3698 by (metis * closedin_def inf_le1 topspace_euclidean_subtopology) |
|
3699 qed |
|
3700 next |
|
3701 assume R [rule_format]: ?rhs |
|
3702 show ?lhs |
|
3703 unfolding continuous_on_open_gen [OF assms] |
|
3704 by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology) |
|
3705 qed |
|
3706 qed |
|
3707 |
|
3708 lemma continuous_closedin_preimage_gen: |
|
3709 assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U" |
|
3710 shows "closedin (subtopology euclidean S) (S \<inter> f -` U)" |
|
3711 using assms continuous_on_closed_gen by blast |
|
3712 |
|
3713 lemma continuous_transform_within_openin: |
|
3714 assumes "continuous (at a within T) f" |
|
3715 and "openin (subtopology euclidean T) S" "a \<in> S" |
|
3716 and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
|
3717 shows "continuous (at a within T) g" |
|
3718 using assms by (simp add: Lim_transform_within_openin continuous_within) |
|
3719 |
|
3720 |
3559 end |
3721 end |