src/HOL/Probability/Caratheodory.thy
changeset 42067 66c8281349ec
parent 42066 6db76c88907a
child 42145 8448713d48b7
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 18:53:05 2011 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 20:06:10 2011 +0100
     1.3 @@ -1,9 +1,18 @@
     1.4 +(*  Title:      HOL/Probability/Caratheodory.thy
     1.5 +    Author:     Lawrence C Paulson
     1.6 +    Author:     Johannes Hölzl, TU München
     1.7 +*)
     1.8 +
     1.9  header {*Caratheodory Extension Theorem*}
    1.10  
    1.11  theory Caratheodory
    1.12    imports Sigma_Algebra Extended_Real_Limits
    1.13  begin
    1.14  
    1.15 +text {*
    1.16 +  Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    1.17 +*}
    1.18 +
    1.19  lemma suminf_extreal_2dimen:
    1.20    fixes f:: "nat \<times> nat \<Rightarrow> extreal"
    1.21    assumes pos: "\<And>p. 0 \<le> f p"
    1.22 @@ -36,8 +45,6 @@
    1.23                       SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    1.24  qed
    1.25  
    1.26 -text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    1.27 -
    1.28  subsection {* Measure Spaces *}
    1.29  
    1.30  record 'a measure_space = "'a algebra" +