src/HOL/Topological_Spaces.thy
changeset 62217 527488dc8b90
parent 62175 8ffc4d0e652d
child 62343 24106dc44def
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jan 20 20:19:05 2016 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jan 22 16:00:03 2016 +0000
     1.3 @@ -1076,6 +1076,9 @@
     1.4  lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
     1.5    using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
     1.6  
     1.7 +lemma lim_const [simp]: "lim (\<lambda>m. a) = a"
     1.8 +  by (simp add: limI)
     1.9 +
    1.10  subsubsection\<open>Increasing and Decreasing Series\<close>
    1.11  
    1.12  lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"