src/HOL/Topological_Spaces.thy
 changeset 56020 f92479477c52 parent 55945 e96383acecf9 child 56166 9a241bc276cd
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Mon Mar 10 17:14:57 2014 +0100
1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Mar 10 20:04:40 2014 +0100
1.3 @@ -1193,26 +1193,25 @@
1.4          The use of disjunction here complicates proofs considerably.
1.5          One alternative is to add a Boolean argument to indicate the direction.
1.6          Another is to develop the notions of increasing and decreasing first.*}
1.7 -  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
1.8 -
1.9 -definition
1.10 -  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.11 -    --{*Increasing sequence*}
1.12 -  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
1.13 -
1.14 -definition
1.15 -  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.16 -    --{*Decreasing sequence*}
1.17 -  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
1.18 +  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
1.19 +
1.20 +abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.21 +  "incseq X \<equiv> mono X"
1.22 +
1.23 +lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
1.24 +  unfolding mono_def ..
1.25 +
1.26 +abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.27 +  "decseq X \<equiv> antimono X"
1.28 +
1.29 +lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
1.30 +  unfolding antimono_def ..
1.31
1.32  definition
1.33    subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
1.34      --{*Definition of subsequence*}
1.35    "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
1.36
1.37 -lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
1.38 -  unfolding mono_def incseq_def by auto
1.39 -
1.40  lemma incseq_SucI:
1.41    "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
1.42    using lift_Suc_mono_le[of X]
```