equal
deleted
inserted
replaced
102 and "(\<lambda>i. positive_integral (f i)) ----> positive_integral u" (is ?ilim) |
102 and "(\<lambda>i. positive_integral (f i)) ----> positive_integral u" (is ?ilim) |
103 proof - |
103 proof - |
104 from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u] |
104 from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u] |
105 show ?ilim using mono lim i by auto |
105 show ?ilim using mono lim i by auto |
106 have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal |
106 have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal |
107 unfolding ext_iff SUPR_fun_expand mono_def by auto |
107 unfolding fun_eq_iff SUPR_fun_expand mono_def by auto |
108 moreover have "(SUP i. f i) \<in> borel_measurable M" |
108 moreover have "(SUP i. f i) \<in> borel_measurable M" |
109 using i by (rule borel_measurable_SUP) |
109 using i by (rule borel_measurable_SUP) |
110 ultimately show "u \<in> borel_measurable M" by simp |
110 ultimately show "u \<in> borel_measurable M" by simp |
111 qed |
111 qed |
112 |
112 |