src/HOL/Limits.thy
changeset 60974 6a6f15d8fbc4
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Limits.thy	Wed Aug 19 15:40:59 2015 +0200
     1.2 +++ b/src/HOL/Limits.thy	Wed Aug 19 19:18:19 2015 +0100
     1.3 @@ -1945,6 +1945,20 @@
     1.4      by auto
     1.5  qed
     1.6  
     1.7 +lemma open_Collect_positive:
     1.8 + fixes f :: "'a::t2_space \<Rightarrow> real"
     1.9 + assumes f: "continuous_on s f"
    1.10 + shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < f x}"
    1.11 + using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"]
    1.12 + by (auto simp: Int_def field_simps)
    1.13 +
    1.14 +lemma open_Collect_less_Int:
    1.15 + fixes f g :: "'a::t2_space \<Rightarrow> real"
    1.16 + assumes f: "continuous_on s f" and g: "continuous_on s g"
    1.17 + shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. f x < g x}"
    1.18 + using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps)
    1.19 +
    1.20 +
    1.21  subsection \<open>Boundedness of continuous functions\<close>
    1.22  
    1.23  text\<open>By bisection, function continuous on closed interval is bounded above\<close>