--- a/src/HOL/Topological_Spaces.thy Sun Feb 19 11:58:51 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Feb 21 15:04:01 2017 +0000
@@ -468,9 +468,9 @@
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
-lemma eventually_eventually:
+lemma eventually_eventually:
"eventually (\<lambda>y. eventually P (nhds y)) (nhds x) = eventually P (nhds x)"
- by (auto simp: eventually_nhds)
+ by (auto simp: eventually_nhds)
lemma (in topological_space) eventually_nhds_in_open:
"open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
@@ -1050,6 +1050,12 @@
definition subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
where "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
+lemma subseq_le_mono: "subseq r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
+ by (simp add: less_mono_imp_le_mono subseq_def)
+
+lemma subseq_id: "subseq id"
+ by (simp add: subseq_def)
+
lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
@@ -1818,6 +1824,12 @@
by (rule continuous_on_closed_Un)
qed
+lemma continuous_on_cases:
+ "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
+ \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
+ continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
+ by (rule continuous_on_If) auto
+
lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
unfolding continuous_on_def by fast