3470 qed |
3470 qed |
3471 |
3471 |
3472 lemma tendsto_Pair [tendsto_intros]: |
3472 lemma tendsto_Pair [tendsto_intros]: |
3473 assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F" |
3473 assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F" |
3474 shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F" |
3474 shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F" |
3475 proof (rule topological_tendstoI) |
3475 unfolding nhds_prod using assms by (rule filterlim_Pair) |
3476 fix S |
|
3477 assume "open S" and "(a, b) \<in> S" |
|
3478 then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" |
|
3479 unfolding open_prod_def by fast |
|
3480 have "eventually (\<lambda>x. f x \<in> A) F" |
|
3481 using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close> |
|
3482 by (rule topological_tendstoD) |
|
3483 moreover |
|
3484 have "eventually (\<lambda>x. g x \<in> B) F" |
|
3485 using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close> |
|
3486 by (rule topological_tendstoD) |
|
3487 ultimately |
|
3488 show "eventually (\<lambda>x. (f x, g x) \<in> S) F" |
|
3489 by (rule eventually_elim2) |
|
3490 (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>]) |
|
3491 qed |
|
3492 |
3476 |
3493 lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" |
3477 lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" |
3494 unfolding continuous_def by (rule tendsto_fst) |
3478 unfolding continuous_def by (rule tendsto_fst) |
3495 |
3479 |
3496 lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" |
3480 lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" |
3623 |
3607 |
3624 lemma isCont_swap[continuous_intros]: "isCont prod.swap a" |
3608 lemma isCont_swap[continuous_intros]: "isCont prod.swap a" |
3625 using continuous_on_eq_continuous_within continuous_on_swap by blast |
3609 using continuous_on_eq_continuous_within continuous_on_swap by blast |
3626 |
3610 |
3627 lemma open_diagonal_complement: |
3611 lemma open_diagonal_complement: |
3628 "open {(x,y) | x y. x \<noteq> (y::('a::t2_space))}" |
3612 "open {(x,y) |x y. x \<noteq> (y::('a::t2_space))}" |
3629 proof (rule topological_space_class.openI) |
3613 proof - |
3630 fix t assume "t \<in> {(x, y) | x y. x \<noteq> (y::'a)}" |
3614 have "open {(x, y). x \<noteq> (y::'a)}" |
3631 then obtain x y where "t = (x,y)" "x \<noteq> y" by blast |
3615 unfolding split_def by (intro open_Collect_neq continuous_intros) |
3632 then obtain U V where *: "open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" |
3616 also have "{(x, y). x \<noteq> (y::'a)} = {(x, y) |x y. x \<noteq> (y::'a)}" |
3633 by (auto simp add: separation_t2) |
3617 by auto |
3634 define T where "T = U \<times> V" |
3618 finally show ?thesis . |
3635 have "open T" using * open_Times T_def by auto |
|
3636 moreover have "t \<in> T" unfolding T_def using \<open>t = (x,y)\<close> * by auto |
|
3637 moreover have "T \<subseteq> {(x, y) | x y. x \<noteq> y}" unfolding T_def using * by auto |
|
3638 ultimately show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {(x, y) | x y. x \<noteq> y}" by auto |
|
3639 qed |
3619 qed |
3640 |
3620 |
3641 lemma closed_diagonal: |
3621 lemma closed_diagonal: |
3642 "closed {y. \<exists> x::('a::t2_space). y = (x,x)}" |
3622 "closed {y. \<exists> x::('a::t2_space). y = (x,x)}" |
3643 proof - |
3623 proof - |
3645 then show ?thesis using open_diagonal_complement closed_Diff by auto |
3625 then show ?thesis using open_diagonal_complement closed_Diff by auto |
3646 qed |
3626 qed |
3647 |
3627 |
3648 lemma open_superdiagonal: |
3628 lemma open_superdiagonal: |
3649 "open {(x,y) | x y. x > (y::'a::{linorder_topology})}" |
3629 "open {(x,y) | x y. x > (y::'a::{linorder_topology})}" |
3650 proof (rule topological_space_class.openI) |
3630 proof - |
3651 fix t assume "t \<in> {(x, y) | x y. y < (x::'a)}" |
3631 have "open {(x, y). x > (y::'a)}" |
3652 then obtain x y where "t = (x, y)" "x > y" by blast |
3632 unfolding split_def by (intro open_Collect_less continuous_intros) |
3653 show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {(x, y) | x y. y < x}" |
3633 also have "{(x, y). x > (y::'a)} = {(x, y) |x y. x > (y::'a)}" |
3654 proof (cases) |
3634 by auto |
3655 assume "\<exists>z. y < z \<and> z < x" |
3635 finally show ?thesis . |
3656 then obtain z where z: "y < z \<and> z < x" by blast |
|
3657 define T where "T = {z<..} \<times> {..<z}" |
|
3658 have "open T" unfolding T_def by (simp add: open_Times) |
|
3659 moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto |
|
3660 moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def by auto |
|
3661 ultimately show ?thesis by auto |
|
3662 next |
|
3663 assume "\<not>(\<exists>z. y < z \<and> z < x)" |
|
3664 then have *: "{x ..} = {y<..}" "{..< x} = {..y}" |
|
3665 using \<open>x > y\<close> apply auto using leI by blast |
|
3666 define T where "T = {x ..} \<times> {.. y}" |
|
3667 then have "T = {y<..} \<times> {..< x}" using * by simp |
|
3668 then have "open T" unfolding T_def by (simp add: open_Times) |
|
3669 moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto |
|
3670 moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def using \<open>x > y\<close> by auto |
|
3671 ultimately show ?thesis by auto |
|
3672 qed |
|
3673 qed |
3636 qed |
3674 |
3637 |
3675 lemma closed_subdiagonal: |
3638 lemma closed_subdiagonal: |
3676 "closed {(x,y) | x y. x \<le> (y::'a::{linorder_topology})}" |
3639 "closed {(x,y) | x y. x \<le> (y::'a::{linorder_topology})}" |
3677 proof - |
3640 proof - |
3679 then show ?thesis using open_superdiagonal closed_Diff by auto |
3642 then show ?thesis using open_superdiagonal closed_Diff by auto |
3680 qed |
3643 qed |
3681 |
3644 |
3682 lemma open_subdiagonal: |
3645 lemma open_subdiagonal: |
3683 "open {(x,y) | x y. x < (y::'a::{linorder_topology})}" |
3646 "open {(x,y) | x y. x < (y::'a::{linorder_topology})}" |
3684 proof (rule topological_space_class.openI) |
3647 proof - |
3685 fix t assume "t \<in> {(x, y) | x y. y > (x::'a)}" |
3648 have "open {(x, y). x < (y::'a)}" |
3686 then obtain x y where "t = (x, y)" "x < y" by blast |
3649 unfolding split_def by (intro open_Collect_less continuous_intros) |
3687 show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {(x, y) | x y. y > x}" |
3650 also have "{(x, y). x < (y::'a)} = {(x, y) |x y. x < (y::'a)}" |
3688 proof (cases) |
3651 by auto |
3689 assume "\<exists>z. y > z \<and> z > x" |
3652 finally show ?thesis . |
3690 then obtain z where z: "y > z \<and> z > x" by blast |
|
3691 define T where "T = {..<z} \<times> {z<..}" |
|
3692 have "open T" unfolding T_def by (simp add: open_Times) |
|
3693 moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto |
|
3694 moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def by auto |
|
3695 ultimately show ?thesis by auto |
|
3696 next |
|
3697 assume "\<not>(\<exists>z. y > z \<and> z > x)" |
|
3698 then have *: "{..x} = {..<y}" "{x<..} = {y..}" |
|
3699 using \<open>x < y\<close> apply auto using leI by blast |
|
3700 define T where "T = {..x} \<times> {y..}" |
|
3701 then have "T = {..<y} \<times> {x<..}" using * by simp |
|
3702 then have "open T" unfolding T_def by (simp add: open_Times) |
|
3703 moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto |
|
3704 moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def using \<open>x < y\<close> by auto |
|
3705 ultimately show ?thesis by auto |
|
3706 qed |
|
3707 qed |
3653 qed |
3708 |
3654 |
3709 lemma closed_superdiagonal: |
3655 lemma closed_superdiagonal: |
3710 "closed {(x,y) | x y. x \<ge> (y::('a::{linorder_topology}))}" |
3656 "closed {(x,y) | x y. x \<ge> (y::('a::{linorder_topology}))}" |
3711 proof - |
3657 proof - |