renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
authorhoelzl
Thu Apr 25 10:35:56 2013 +0200 (2013-04-25)
changeset 51774916271d52466
parent 51773 9328c6681f3c
child 51775 408d937c9486
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
NEWS
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Wed Apr 24 13:28:30 2013 +0200
     1.2 +++ b/NEWS	Thu Apr 25 10:35:56 2013 +0200
     1.3 @@ -133,7 +133,8 @@
     1.4  
     1.5   - connected from Multivariate_Analysis. Use it to prove the
     1.6     intermediate value theorem. Show connectedness of intervals on order
     1.7 -   topologies which are a inner dense, conditionally-complete linorder.
     1.8 +   topologies which are a inner dense, conditionally-complete linorder
     1.9 +   (named connected_linorder_topology).
    1.10  
    1.11   - first_countable_topology from Multivariate_Analysis. Is used to
    1.12     show equivalence of properties on the neighbourhood filter of x and on
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Apr 24 13:28:30 2013 +0200
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Apr 25 10:35:56 2013 +0200
     2.3 @@ -1572,7 +1572,7 @@
     2.4  
     2.5  subsubsection "Topological space"
     2.6  
     2.7 -instantiation ereal :: linorder_topology
     2.8 +instantiation ereal :: connected_linorder_topology
     2.9  begin
    2.10  
    2.11  definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
     3.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
     3.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     3.3 @@ -860,7 +860,7 @@
     3.4    qed
     3.5  qed
     3.6  
     3.7 -instance real :: linear_continuum_topology ..
     3.8 +instance real :: connected_linorder_topology ..
     3.9  
    3.10  lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
    3.11  lemmas open_real_lessThan = open_lessThan[where 'a=real]
     4.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
     4.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     4.3 @@ -2079,7 +2079,7 @@
     4.4  
     4.5  section {* Connectedness *}
     4.6  
     4.7 -class linear_continuum_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     4.8 +class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     4.9  begin
    4.10  
    4.11  lemma Inf_notin_open:
    4.12 @@ -2111,7 +2111,7 @@
    4.13  end
    4.14  
    4.15  lemma connectedI_interval:
    4.16 -  fixes U :: "'a :: linear_continuum_topology set"
    4.17 +  fixes U :: "'a :: connected_linorder_topology set"
    4.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"
    4.19    shows "connected U"
    4.20  proof (rule connectedI)
    4.21 @@ -2154,35 +2154,35 @@
    4.22  qed
    4.23  
    4.24  lemma connected_iff_interval:
    4.25 -  fixes U :: "'a :: linear_continuum_topology set"
    4.26 +  fixes U :: "'a :: connected_linorder_topology set"
    4.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)"
    4.28    by (auto intro: connectedI_interval dest: connectedD_interval)
    4.29  
    4.30 -lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    4.31 +lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
    4.32    unfolding connected_iff_interval by auto
    4.33  
    4.34 -lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
    4.35 +lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
    4.36    unfolding connected_iff_interval by auto
    4.37  
    4.38 -lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
    4.39 +lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
    4.40    unfolding connected_iff_interval by auto
    4.41  
    4.42 -lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
    4.43 +lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
    4.44    unfolding connected_iff_interval by auto
    4.45  
    4.46 -lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
    4.47 +lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
    4.48    unfolding connected_iff_interval by auto
    4.49  
    4.50 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
    4.51 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
    4.52    unfolding connected_iff_interval by auto
    4.53  
    4.54 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
    4.55 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
    4.56    unfolding connected_iff_interval by auto
    4.57  
    4.58 -lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
    4.59 +lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
    4.60    unfolding connected_iff_interval by auto
    4.61  
    4.62 -lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
    4.63 +lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
    4.64    unfolding connected_iff_interval by auto
    4.65  
    4.66  lemma connected_contains_Ioo: 
    4.67 @@ -2193,7 +2193,7 @@
    4.68  subsection {* Intermediate Value Theorem *}
    4.69  
    4.70  lemma IVT':
    4.71 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    4.72 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    4.73    assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
    4.74    assumes *: "continuous_on {a .. b} f"
    4.75    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    4.76 @@ -2206,7 +2206,7 @@
    4.77  qed
    4.78  
    4.79  lemma IVT2':
    4.80 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    4.81 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    4.82    assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
    4.83    assumes *: "continuous_on {a .. b} f"
    4.84    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    4.85 @@ -2219,17 +2219,17 @@
    4.86  qed
    4.87  
    4.88  lemma IVT:
    4.89 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    4.90 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    4.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"
    4.92    by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
    4.93  
    4.94  lemma IVT2:
    4.95 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    4.96 +  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    4.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"
    4.98    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
    4.99  
   4.100  lemma continuous_inj_imp_mono:
   4.101 -  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   4.102 +  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   4.103    assumes x: "a < x" "x < b"
   4.104    assumes cont: "continuous_on {a..b} f"
   4.105    assumes inj: "inj_on f {a..b}"