added lemma
authornipkow
Fri Jan 19 08:28:08 2018 +0100 (18 months ago)
changeset 674567895c159d7b1
parent 67455 fe6bcf0137b4
child 67457 4b921bb461f6
added lemma
CONTRIBUTORS
src/HOL/Library/Extended_Nonnegative_Real.thy
     1.1 --- a/CONTRIBUTORS	Thu Jan 18 17:04:35 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Fri Jan 19 08:28:08 2018 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* January 2018: Sebastien Gouezel
     1.8 +  Various small additions to HOL-Analysis
     1.9 +
    1.10  * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
    1.11    A new conditional parametricity prover.
    1.12  
     2.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jan 18 17:04:35 2018 +0100
     2.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 19 08:28:08 2018 +0100
     2.3 @@ -923,6 +923,9 @@
     2.4  lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
     2.5    by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
     2.6  
     2.7 +lemma enn2ereal_e2ennreal: "x \<ge> 0 \<Longrightarrow> enn2ereal (e2ennreal x) = x"
     2.8 +by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)
     2.9 +
    2.10  lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
    2.11  by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
    2.12