src/HOL/Analysis/Borel_Space.thy
changeset 67685 bdff8bf0a75b
parent 67399 eab6ce8368fa
child 68635 8094b853a92f
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Feb 20 22:25:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Thu Feb 22 15:17:25 2018 +0100
     1.3 @@ -242,6 +242,11 @@
     1.4    shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
     1.5    by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
     1.6  
     1.7 +lemma closed_subset_contains_Sup:
     1.8 +  fixes A C :: "real set"
     1.9 +  shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
    1.10 +  by (metis closure_contains_Sup closure_minimal subset_eq)
    1.11 +
    1.12  lemma deriv_nonneg_imp_mono:
    1.13    assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
    1.14    assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"