equal
deleted
inserted
replaced
1169 then show "eventually (\<lambda>x. min (X x) (Y x) < a) net" |
1169 then show "eventually (\<lambda>x. min (X x) (Y x) < a) net" |
1170 using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] |
1170 using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] |
1171 by (auto simp: min_less_iff_disj elim: eventually_elim1) |
1171 by (auto simp: min_less_iff_disj elim: eventually_elim1) |
1172 qed |
1172 qed |
1173 |
1173 |
1174 lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)" |
1174 lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)" |
1175 unfolding tendsto_def eventually_at_topological by auto |
1175 unfolding tendsto_def eventually_at_topological by auto |
1176 |
1176 |
1177 lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F" |
1177 lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F" |
1178 by (simp add: tendsto_def) |
1178 by (simp add: tendsto_def) |
1179 |
1179 |
1180 lemma (in t2_space) tendsto_unique: |
1180 lemma (in t2_space) tendsto_unique: |
1181 assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F" |
1181 assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F" |
1182 shows "a = b" |
1182 shows "a = b" |
1200 by (simp add: trivial_limit_def) |
1200 by (simp add: trivial_limit_def) |
1201 qed |
1201 qed |
1202 |
1202 |
1203 lemma (in t2_space) tendsto_const_iff: |
1203 lemma (in t2_space) tendsto_const_iff: |
1204 assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b" |
1204 assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b" |
1205 by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) |
1205 by (auto intro!: tendsto_unique [OF assms tendsto_const]) |
1206 |
1206 |
1207 lemma increasing_tendsto: |
1207 lemma increasing_tendsto: |
1208 fixes f :: "_ \<Rightarrow> 'a::order_topology" |
1208 fixes f :: "_ \<Rightarrow> 'a::order_topology" |
1209 assumes bdd: "eventually (\<lambda>n. f n \<le> l) F" |
1209 assumes bdd: "eventually (\<lambda>n. f n \<le> l) F" |
1210 and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F" |
1210 and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F" |
1687 "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)" |
1687 "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)" |
1688 using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) |
1688 using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) |
1689 |
1689 |
1690 lemma LIMSEQ_le_const2: |
1690 lemma LIMSEQ_le_const2: |
1691 "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" |
1691 "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" |
1692 by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const) |
1692 by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto |
1693 |
1693 |
1694 lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)" |
1694 lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)" |
1695 by (simp add: convergent_def) |
1695 by (simp add: convergent_def) |
1696 |
1696 |
1697 lemma convergentI: "(X ----> L) ==> convergent X" |
1697 lemma convergentI: "(X ----> L) ==> convergent X" |
2115 with closed show ?thesis |
2115 with closed show ?thesis |
2116 by (rule continuous_on_closed_Un) |
2116 by (rule continuous_on_closed_Un) |
2117 qed |
2117 qed |
2118 |
2118 |
2119 lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)" |
2119 lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)" |
2120 unfolding continuous_on_def by (fast intro: tendsto_ident_at) |
2120 unfolding continuous_on_def by fast |
2121 |
2121 |
2122 lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)" |
2122 lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)" |
2123 unfolding continuous_on_def by (auto intro: tendsto_const) |
2123 unfolding continuous_on_def by auto |
2124 |
2124 |
2125 lemma continuous_on_compose[continuous_intros]: |
2125 lemma continuous_on_compose[continuous_intros]: |
2126 "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)" |
2126 "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)" |
2127 unfolding continuous_on_topological by simp metis |
2127 unfolding continuous_on_topological by simp metis |
2128 |
2128 |