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