--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100
@@ -2090,6 +2090,14 @@
lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
by (simp add: is_interval_convex_1)
+lemma [simp]:
+ fixes r s::real
+ shows is_interval_io: "is_interval {..<r}"
+ and is_interval_oi: "is_interval {r<..}"
+ and is_interval_oo: "is_interval {r<..<s}"
+ and is_interval_oc: "is_interval {r<..s}"
+ and is_interval_co: "is_interval {r..<s}"
+ by (simp_all add: is_interval_convex_1)
subsection%unimportant \<open>Another intermediate value theorem formulation\<close>