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}"
```