equal
deleted
inserted
replaced
1073 lemma limI: "X \<longlonglongrightarrow> L ==> lim X = L" |
1073 lemma limI: "X \<longlonglongrightarrow> L ==> lim X = L" |
1074 by (rule tendsto_Lim) (rule trivial_limit_sequentially) |
1074 by (rule tendsto_Lim) (rule trivial_limit_sequentially) |
1075 |
1075 |
1076 lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x" |
1076 lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x" |
1077 using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff) |
1077 using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff) |
|
1078 |
|
1079 lemma lim_const [simp]: "lim (\<lambda>m. a) = a" |
|
1080 by (simp add: limI) |
1078 |
1081 |
1079 subsubsection\<open>Increasing and Decreasing Series\<close> |
1082 subsubsection\<open>Increasing and Decreasing Series\<close> |
1080 |
1083 |
1081 lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)" |
1084 lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)" |
1082 by (metis incseq_def LIMSEQ_le_const) |
1085 by (metis incseq_def LIMSEQ_le_const) |