src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -1501,7 +1501,7 @@
     1.4  
     1.5  lemma ennreal_SUP_add:
     1.6    fixes f g :: "nat \<Rightarrow> ennreal"
     1.7 -  shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
     1.8 +  shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
     1.9    unfolding incseq_def le_fun_def
    1.10    by transfer
    1.11       (simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)
    1.12 @@ -1591,7 +1591,7 @@
    1.13    done
    1.14  
    1.15  lemma ennreal_SUP_countable_SUP:
    1.16 -  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
    1.17 +  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> Sup (g ` A) = Sup (f ` UNIV)"
    1.18    using ennreal_Sup_countable_SUP [of "g`A"] by auto
    1.19  
    1.20  lemma of_nat_tendsto_top_ennreal: "(\<lambda>n::nat. of_nat n :: ennreal) \<longlonglongrightarrow> top"