equal
deleted
inserted
replaced
219 lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
219 lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
220 by (blast intro: reals_complete Bseq_isUb) |
220 by (blast intro: reals_complete Bseq_isUb) |
221 |
221 |
222 lemma isLub_mono_imp_LIMSEQ: |
222 lemma isLub_mono_imp_LIMSEQ: |
223 fixes X :: "nat \<Rightarrow> real" |
223 fixes X :: "nat \<Rightarrow> real" |
224 assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *) |
224 assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use \<open>range X\<close> *) |
225 assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
225 assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
226 shows "X \<longlonglongrightarrow> u" |
226 shows "X \<longlonglongrightarrow> u" |
227 proof - |
227 proof - |
228 have "X \<longlonglongrightarrow> (SUP i. X i)" |
228 have "X \<longlonglongrightarrow> (SUP i. X i)" |
229 using u[THEN isLubD1] X |
229 using u[THEN isLubD1] X |