src/HOL/Topological_Spaces.thy
 changeset 60720 8c99fa3b7c44 parent 60585 48fdff264eb2 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jul 13 19:25:58 2015 +0200
1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Jul 14 13:37:44 2015 +0200
1.3 @@ -1423,6 +1423,61 @@
1.4    "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
1.5    using continuous_on_compose[of s f g] by (simp add: comp_def)
1.6
1.7 +lemma continuous_on_generate_topology:
1.8 +  assumes *: "open = generate_topology X"
1.9 +  assumes **: "\<And>B. B \<in> X \<Longrightarrow> \<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
1.10 +  shows "continuous_on A f"
1.11 +  unfolding continuous_on_open_invariant
1.12 +proof safe
1.13 +  fix B :: "'a set" assume "open B" then show "\<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
1.14 +    unfolding *
1.15 +  proof induction
1.16 +    case (UN K)
1.17 +    then obtain C where "\<And>k. k \<in> K \<Longrightarrow> open (C k)" "\<And>k. k \<in> K \<Longrightarrow> C k \<inter> A = f -` k \<inter> A"
1.18 +      by metis
1.19 +    then show ?case
1.20 +      by (intro exI[of _ "\<Union>k\<in>K. C k"]) blast
1.21 +  qed (auto intro: **)
1.22 +qed
1.23 +
1.24 +lemma continuous_onI_mono:
1.25 +  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::{dense_order, linorder_topology}"
1.26 +  assumes "open (f`A)"
1.27 +  assumes mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
1.28 +  shows "continuous_on A f"
1.29 +proof (rule continuous_on_generate_topology[OF open_generated_order], safe)
1.30 +  have monoD: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x < f y \<Longrightarrow> x < y"
1.31 +    by (auto simp: not_le[symmetric] mono)
1.32 +
1.33 +  { fix a b assume "a \<in> A" "f a < b"
1.34 +    moreover
1.35 +    with open_right[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "f a < y" "{f a ..< y} \<subseteq> f`A"
1.36 +      by auto
1.37 +    moreover then obtain z where "f a < z" "z < min b y"
1.38 +      using dense[of "f a" "min b y"] \<open>f a < y\<close> \<open>f a < b\<close> by auto
1.39 +    moreover then obtain c where "z = f c" "c \<in> A"
1.40 +      using \<open>{f a ..< y} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
1.41 +    ultimately have "\<exists>x. x \<in> A \<and> f x < b \<and> a < x"
1.42 +      by (auto intro!: exI[of _ c] simp: monoD) }
1.43 +  then show "\<exists>C. open C \<and> C \<inter> A = f -` {..<b} \<inter> A" for b
1.44 +    by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. f x < b}. {..< x})"])
1.45 +       (auto intro: le_less_trans[OF mono] less_imp_le)
1.46 +
1.47 +  { fix a b assume "a \<in> A" "b < f a"
1.48 +    moreover
1.49 +    with open_left[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "y < f a" "{y <.. f a} \<subseteq> f`A"
1.50 +      by auto
1.51 +    moreover then obtain z where "max b y < z" "z < f a"
1.52 +      using dense[of "max b y" "f a"] \<open>y < f a\<close> \<open>b < f a\<close> by auto
1.53 +    moreover then obtain c where "z = f c" "c \<in> A"
1.54 +      using \<open>{y <.. f a} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
1.55 +    ultimately have "\<exists>x. x \<in> A \<and> b < f x \<and> x < a"
1.56 +      by (auto intro!: exI[of _ c] simp: monoD) }
1.57 +  then show "\<exists>C. open C \<and> C \<inter> A = f -` {b <..} \<inter> A" for b
1.58 +    by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. b < f x}. {x <..})"])
1.59 +       (auto intro: less_le_trans[OF _ mono] less_imp_le)
1.60 +qed
1.61 +
1.62  subsubsection {* Continuity at a point *}
1.63
1.64  definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
```