src/HOL/Topological_Spaces.thy
changeset 51774 916271d52466
parent 51773 9328c6681f3c
child 51775 408d937c9486
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     1.3 @@ -2079,7 +2079,7 @@
     1.4  
     1.5  section {* Connectedness *}
     1.6  
     1.7 -class linear_continuum_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     1.8 +class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     1.9  begin
    1.10  
    1.11  lemma Inf_notin_open:
    1.12 @@ -2111,7 +2111,7 @@
    1.13  end
    1.14  
    1.15  lemma connectedI_interval:
    1.16 -  fixes U :: "'a :: linear_continuum_topology set"
    1.17 +  fixes U :: "'a :: connected_linorder_topology set"
    1.18    assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    1.19    shows "connected U"
    1.20  proof (rule connectedI)
    1.21 @@ -2154,35 +2154,35 @@
    1.22  qed
    1.23  
    1.24  lemma connected_iff_interval:
    1.25 -  fixes U :: "'a :: linear_continuum_topology set"
    1.26 +  fixes U :: "'a :: connected_linorder_topology set"
    1.27    shows "connected U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>y\<in>U. \<forall>z. x \<le> z \<longrightarrow> z \<le> y \<longrightarrow> z \<in> U)"
    1.28    by (auto intro: connectedI_interval dest: connectedD_interval)
    1.29  
    1.30 -lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    1.31 +lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
    1.32    unfolding connected_iff_interval by auto
    1.33  
    1.34 -lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
    1.35 +lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
    1.36    unfolding connected_iff_interval by auto
    1.37  
    1.38 -lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
    1.39 +lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
    1.40    unfolding connected_iff_interval by auto
    1.41  
    1.42 -lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
    1.43 +lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
    1.44    unfolding connected_iff_interval by auto
    1.45  
    1.46 -lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
    1.47 +lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
    1.48    unfolding connected_iff_interval by auto
    1.49  
    1.50 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
    1.51 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
    1.52    unfolding connected_iff_interval by auto
    1.53  
    1.54 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
    1.55 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
    1.56    unfolding connected_iff_interval by auto
    1.57  
    1.58 -lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
    1.59 +lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
    1.60    unfolding connected_iff_interval by auto
    1.61  
    1.62 -lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
    1.63 +lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
    1.64    unfolding connected_iff_interval by auto
    1.65  
    1.66  lemma connected_contains_Ioo: 
    1.67 @@ -2193,7 +2193,7 @@
    1.68  subsection {* Intermediate Value Theorem *}
    1.69  
    1.70  lemma IVT':
    1.71 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.72 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.73    assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
    1.74    assumes *: "continuous_on {a .. b} f"
    1.75    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.76 @@ -2206,7 +2206,7 @@
    1.77  qed
    1.78  
    1.79  lemma IVT2':
    1.80 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.81 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.82    assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
    1.83    assumes *: "continuous_on {a .. b} f"
    1.84    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.85 @@ -2219,17 +2219,17 @@
    1.86  qed
    1.87  
    1.88  lemma IVT:
    1.89 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.90 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.91    shows "f a \<le> y \<Longrightarrow> y \<le> f b \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.92    by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
    1.93  
    1.94  lemma IVT2:
    1.95 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.96 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.97    shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.98    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
    1.99  
   1.100  lemma continuous_inj_imp_mono:
   1.101 -  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   1.102 +  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   1.103    assumes x: "a < x" "x < b"
   1.104    assumes cont: "continuous_on {a..b} f"
   1.105    assumes inj: "inj_on f {a..b}"