src/HOL/Topological_Spaces.thy
 changeset 51775 408d937c9486 parent 51774 916271d52466 child 52265 bb907eba5902
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
1.3 @@ -2079,7 +2079,7 @@
1.4
1.5  section {* Connectedness *}
1.6
1.7 -class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
1.8 +class linear_continuum_topology = linorder_topology + linear_continuum
1.9  begin
1.10
1.11  lemma Inf_notin_open:
1.12 @@ -2110,8 +2110,17 @@
1.13
1.14  end
1.15
1.16 +instance linear_continuum_topology \<subseteq> perfect_space
1.17 +proof
1.18 +  fix x :: 'a
1.19 +  from ex_gt_or_lt [of x] guess y ..
1.20 +  with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
1.21 +  show "\<not> open {x}"
1.22 +    by auto
1.23 +qed
1.24 +
1.25  lemma connectedI_interval:
1.26 -  fixes U :: "'a :: connected_linorder_topology set"
1.27 +  fixes U :: "'a :: linear_continuum_topology set"
1.28    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.29    shows "connected U"
1.30  proof (rule connectedI)
1.31 @@ -2154,35 +2163,35 @@
1.32  qed
1.33
1.34  lemma connected_iff_interval:
1.35 -  fixes U :: "'a :: connected_linorder_topology set"
1.36 +  fixes U :: "'a :: linear_continuum_topology set"
1.37    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.38    by (auto intro: connectedI_interval dest: connectedD_interval)
1.39
1.40 -lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
1.41 +lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
1.42    unfolding connected_iff_interval by auto
1.43
1.44 -lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
1.45 +lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
1.46    unfolding connected_iff_interval by auto
1.47
1.48 -lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
1.49 +lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
1.50    unfolding connected_iff_interval by auto
1.51
1.52 -lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
1.53 +lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
1.54    unfolding connected_iff_interval by auto
1.55
1.56 -lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
1.57 +lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
1.58    unfolding connected_iff_interval by auto
1.59
1.60 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
1.61 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
1.62    unfolding connected_iff_interval by auto
1.63
1.64 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
1.65 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
1.66    unfolding connected_iff_interval by auto
1.67
1.68 -lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
1.69 +lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
1.70    unfolding connected_iff_interval by auto
1.71
1.72 -lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
1.73 +lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
1.74    unfolding connected_iff_interval by auto
1.75
1.76  lemma connected_contains_Ioo:
1.77 @@ -2193,7 +2202,7 @@
1.78  subsection {* Intermediate Value Theorem *}
1.79
1.80  lemma IVT':
1.81 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
1.82 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
1.83    assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
1.84    assumes *: "continuous_on {a .. b} f"
1.85    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
1.86 @@ -2206,7 +2215,7 @@
1.87  qed
1.88
1.89  lemma IVT2':
1.90 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
1.91 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
1.92    assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
1.93    assumes *: "continuous_on {a .. b} f"
1.94    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
1.95 @@ -2219,17 +2228,17 @@
1.96  qed
1.97
1.98  lemma IVT:
1.99 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
1.100 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
1.101    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.102    by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
1.103
1.104  lemma IVT2:
1.105 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
1.106 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
1.107    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.108    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
1.109
1.110  lemma continuous_inj_imp_mono:
1.111 -  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
1.112 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
1.113    assumes x: "a < x" "x < b"
1.114    assumes cont: "continuous_on {a..b} f"
1.115    assumes inj: "inj_on f {a..b}"
```