# HG changeset patch
# User nipkow
# Date 1535035519 -7200
# Node ID 63e84bd8e1f68f1ef32b15ca3cc61f76db6a183e
# Parent  462226db648aef8aa75267f5d034f60d6bf02a6e
moved lemma from AFP

diff -r 462226db648a -r 63e84bd8e1f6 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 23 14:49:36 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 23 16:45:19 2018 +0200
@@ -2026,6 +2026,14 @@
   ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp
 qed
 
+lemma integrable_MIN:
+  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
+  shows "integrable M (\<lambda>x. MIN i\<in>I. f i x)"
+using integrable_Min[of I M f, OF assms]
+by(simp add: Setcompr_eq_image)
+
 lemma integrable_Max:
   fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
   assumes "finite I" "I \<noteq> {}"
@@ -2043,6 +2051,14 @@
   ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp
 qed
 
+lemma integrable_MAX:
+  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
+  shows "integrable M (\<lambda>x. MAX i\<in>I. f i x)"
+using integrable_Max[of I M f, OF assms]
+by(simp add: Setcompr_eq_image)
+
 lemma integral_Markov_inequality:
   assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
   shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"