--- a/src/HOL/Complex.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Complex.thy Mon Mar 31 21:15:26 2014 +0200
@@ -232,6 +232,8 @@
abbreviation complex_of_real :: "real \<Rightarrow> complex"
where "complex_of_real \<equiv> of_real"
+declare [[coercion complex_of_real]]
+
lemma complex_of_real_def: "complex_of_real r = Complex r 0"
by (simp add: of_real_def complex_scaleR_def)
--- a/src/HOL/Limits.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Limits.thy Mon Mar 31 21:15:26 2014 +0200
@@ -1164,6 +1164,25 @@
using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
unfolding filterlim_uminus_at_bot by simp
+lemma filterlim_pow_at_top:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "0 < n" and f: "LIM x F. f x :> at_top"
+ shows "LIM x F. (f x)^n :: real :> at_top"
+using `0 < n` proof (induct n)
+ case (Suc n) with f show ?case
+ by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top)
+qed simp
+
+lemma filterlim_pow_at_bot_even:
+ fixes f :: "real \<Rightarrow> real"
+ shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top"
+ using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_top)
+
+lemma filterlim_pow_at_bot_odd:
+ fixes f :: "real \<Rightarrow> real"
+ shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
+ using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
+
lemma filterlim_tendsto_add_at_top:
assumes f: "(f ---> c) F"
assumes g: "LIM x F. g x :> at_top"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 31 21:15:26 2014 +0200
@@ -6,7 +6,6 @@
theory Complex_Analysis_Basics
imports "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
-
begin
subsection {*Complex number lemmas *}
@@ -28,11 +27,11 @@
done
qed
-lemma continuous_Re: "continuous_on UNIV Re"
+lemma continuous_Re: "continuous_on X Re"
by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re
continuous_on_cong continuous_on_id)
-lemma continuous_Im: "continuous_on UNIV Im"
+lemma continuous_Im: "continuous_on X Im"
by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im
continuous_on_cong continuous_on_id)
@@ -52,95 +51,29 @@
apply (simp add: algebra_simps of_nat_mult)
done
-lemma open_halfspace_Re_lt: "open {z. Re(z) < b}"
-proof -
- have "{z. Re(z) < b} = Re -`{..<b}"
- by blast
- then show ?thesis
- by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Re_gt: "open {z. Re(z) > b}"
-proof -
- have "{z. Re(z) > b} = Re -`{b<..}"
- by blast
- then show ?thesis
- by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
-proof -
- have "{z. Re(z) \<ge> b} = - {z. Re(z) < b}"
- by auto
- then show ?thesis
- by (simp add: closed_def open_halfspace_Re_lt)
-qed
-
-lemma closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
-proof -
- have "{z. Re(z) \<le> b} = - {z. Re(z) > b}"
- by auto
- then show ?thesis
- by (simp add: closed_def open_halfspace_Re_gt)
-qed
-
-lemma closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
-proof -
- have "{z. Re(z) = b} = {z. Re(z) \<le> b} \<inter> {z. Re(z) \<ge> b}"
- by auto
- then show ?thesis
- by (auto simp: closed_Int closed_halfspace_Re_le closed_halfspace_Re_ge)
-qed
-
-lemma open_halfspace_Im_lt: "open {z. Im(z) < b}"
-proof -
- have "{z. Im(z) < b} = Im -`{..<b}"
- by blast
- then show ?thesis
- by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Im_gt: "open {z. Im(z) > b}"
-proof -
- have "{z. Im(z) > b} = Im -`{b<..}"
- by blast
- then show ?thesis
- by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
-proof -
- have "{z. Im(z) \<ge> b} = - {z. Im(z) < b}"
- by auto
- then show ?thesis
- by (simp add: closed_def open_halfspace_Im_lt)
-qed
-
-lemma closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
-proof -
- have "{z. Im(z) \<le> b} = - {z. Im(z) > b}"
- by auto
- then show ?thesis
- by (simp add: closed_def open_halfspace_Im_gt)
-qed
-
-lemma closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
-proof -
- have "{z. Im(z) = b} = {z. Im(z) \<le> b} \<inter> {z. Im(z) \<ge> b}"
- by auto
- then show ?thesis
- by (auto simp: closed_Int closed_halfspace_Im_le closed_halfspace_Im_ge)
-qed
+lemma
+ shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
+ and open_halfspace_Re_gt: "open {z. Re(z) > b}"
+ and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
+ and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
+ and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
+ and open_halfspace_Im_lt: "open {z. Im(z) < b}"
+ and open_halfspace_Im_gt: "open {z. Im(z) > b}"
+ and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
+ and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
+ and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
+ by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
+ isCont_Im isCont_ident isCont_const)+
lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
lemma closed_complex_Reals: "closed (Reals :: complex set)"
proof -
- have "-(Reals :: complex set) = {z. Im(z) < 0} \<union> {z. 0 < Im(z)}"
+ have "(Reals :: complex set) = {z. Im z = 0}"
by (auto simp: complex_is_Real_iff)
then show ?thesis
- by (metis closed_def open_Un open_halfspace_Im_gt open_halfspace_Im_lt)
+ by (metis closed_halfspace_Im_eq)
qed
@@ -218,25 +151,8 @@
lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
- assumes "uniformly_continuous_on s f"
- shows "uniformly_continuous_on s (\<lambda>x. f x * c)"
-proof (cases "c=0")
- case True then show ?thesis
- by (simp add: uniformly_continuous_on_const)
-next
- case False show ?thesis
- apply (rule bounded_linear.uniformly_continuous_on)
- apply (metis bounded_linear_ident)
- using assms
- apply (auto simp: uniformly_continuous_on_def dist_norm)
- apply (drule_tac x = "e / norm c" in spec, auto)
- apply (metis divide_pos_pos zero_less_norm_iff False)
- apply (rule_tac x=d in exI, auto)
- apply (drule_tac x = x in bspec, assumption)
- apply (drule_tac x = "x'" in bspec)
- apply (auto simp: False less_divide_eq)
- by (metis dual_order.strict_trans2 left_diff_distrib norm_mult_ineq)
-qed
+ shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
+ by (metis bounded_linear.uniformly_continuous_on[of "\<lambda>x. x * c"] bounded_linear_mult_left)
lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
@@ -259,62 +175,6 @@
lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
by auto
-lemma has_derivative_zero_constant:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "convex s"
- and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
- shows "\<exists>c. \<forall>x\<in>s. f x = c"
-proof (cases "s={}")
- case False
- then obtain x where "x \<in> s"
- by auto
- have d0': "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
- by (metis d0)
- have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
- proof -
- case goal1
- then show ?case
- using differentiable_bound[OF assms(1) d0', of 0 x y] and `x \<in> s`
- unfolding onorm_zero
- by auto
- qed
- then show ?thesis
- by metis
-next
- case True
- then show ?thesis by auto
-qed
-
-lemma has_derivative_zero_unique:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "convex s"
- and "\<And>x. x\<in>s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
- and "a \<in> s"
- and "x \<in> s"
- shows "f x = f a"
- using assms
- by (metis has_derivative_zero_constant)
-
-lemma has_derivative_zero_connected_constant:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
- assumes "connected s"
- and "open s"
- and "finite k"
- and "continuous_on s f"
- and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
- obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
-proof (cases "s = {}")
- case True
- then show ?thesis
-by (metis empty_iff that)
-next
- case False
- then obtain c where "c \<in> s"
- by (metis equals0I)
- then show ?thesis
- by (metis has_derivative_zero_unique_strong_connected assms that)
-qed
-
lemma DERIV_zero_connected_constant:
fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
assumes "connected s"
@@ -342,8 +202,8 @@
and "a \<in> s"
and "x \<in> s"
shows "f x = f a"
-apply (rule has_derivative_zero_unique [where f=f, OF assms(1) _ assms(3,4)])
-by (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
+ by (rule has_derivative_zero_unique [where f=f, OF assms(1,3) refl _ assms(4)])
+ (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
lemma DERIV_zero_connected_unique:
fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
@@ -353,7 +213,7 @@
and "a \<in> s"
and "x \<in> s"
shows "f x = f a"
- apply (rule Integration.has_derivative_zero_unique_strong_connected [of s "{}" f])
+ apply (rule has_derivative_zero_unique_strong_connected [of s "{}" f])
using assms
apply auto
apply (metis DERIV_continuous_on)
@@ -365,7 +225,7 @@
and "\<And>x. x\<in>s \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
shows "(g has_field_derivative f') (at a within s)"
using assms unfolding has_field_derivative_def
- by (blast intro: Derivative.has_derivative_transform_within)
+ by (blast intro: has_derivative_transform_within)
lemma DERIV_transform_within_open:
assumes "DERIV f a :> f'"
@@ -1177,21 +1037,18 @@
lemma continuous_on_cnj: "continuous_on s cnj"
by (metis bounded_linear_cnj linear_continuous_on)
-subsection{*Some limit theorems about real part of real series etc.*}
+subsection {*Some limit theorems about real part of real series etc.*}
lemma real_lim:
fixes l::complex
- assumes "(f ---> l) F" and " ~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
+ assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
shows "l \<in> \<real>"
-proof -
- have 1: "((\<lambda>i. Im (f i)) ---> Im l) F"
- by (metis assms(1) tendsto_Im)
- then have "((\<lambda>i. Im (f i)) ---> 0) F" using assms
- by (metis (mono_tags, lifting) Lim_eventually complex_is_Real_iff eventually_mono)
- then show ?thesis using 1
- by (metis 1 assms(2) complex_is_Real_iff tendsto_unique)
-qed
-
+proof (rule Lim_in_closed_set)
+ show "closed (\<real>::complex set)"
+ by (rule closed_complex_Reals)
+ show "eventually (\<lambda>x. f x \<in> \<real>) F"
+ using assms(3, 4) by (auto intro: eventually_mono)
+qed fact+
lemma real_lim_sequentially:
fixes l::complex
shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
@@ -1209,14 +1066,6 @@
by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
-lemma norm_setsum_bound:
- fixes n::nat
- shows" \<lbrakk>\<And>n. N \<le> n \<Longrightarrow> norm (f n) \<le> g n; N \<le> m\<rbrakk>
- \<Longrightarrow> norm (setsum f {m..<n}) \<le> setsum g {m..<n}"
-apply (induct n, auto)
-by (metis dual_order.trans le_cases le_neq_implies_less norm_triangle_mono)
-
-
(*MOVE? But not to Finite_Cartesian_Product*)
lemma sums_vec_nth :
assumes "f sums a"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 31 21:15:26 2014 +0200
@@ -883,25 +883,14 @@
assumes "convex s"
and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
shows "\<exists>c. \<forall>x\<in>s. f x = c"
-proof (cases "s={}")
- case False
- then obtain x where "x \<in> s"
- by auto
- have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
- proof -
- case goal1
- then show ?case
- using differentiable_bound[OF assms(1-2), of 0 x y] and `x \<in> s`
- unfolding onorm_zero
- by auto
- qed
+proof -
+ { fix x y assume "x \<in> s" "y \<in> s"
+ then have "norm (f x - f y) \<le> 0 * norm (x - y)"
+ using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
+ then have "f x = f y"
+ by simp }
then show ?thesis
- apply (rule_tac x="f x" in exI)
- apply auto
- done
-next
- case True
- then show ?thesis by auto
+ by metis
qed
lemma has_derivative_zero_unique:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 31 21:15:26 2014 +0200
@@ -8869,6 +8869,26 @@
using `x \<in> s` `f c = y` `c \<in> s` by auto
qed
+lemma has_derivative_zero_connected_constant:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+ assumes "connected s"
+ and "open s"
+ and "finite k"
+ and "continuous_on s f"
+ and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
+ obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
+proof (cases "s = {}")
+ case True
+ then show ?thesis
+by (metis empty_iff that)
+next
+ case False
+ then obtain c where "c \<in> s"
+ by (metis equals0I)
+ then show ?thesis
+ by (metis has_derivative_zero_unique_strong_connected assms that)
+qed
+
subsection {* Integrating characteristic function of an interval *}
--- a/src/HOL/Set_Interval.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Set_Interval.thy Mon Mar 31 21:15:26 2014 +0200
@@ -414,6 +414,11 @@
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
+lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:
+ "{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+ using dense[of "a" "min c b"] dense[of "max a d" "b"]
+ by (force simp: subset_eq Ball_def not_less[symmetric])
+
end
context no_top
@@ -463,6 +468,88 @@
by (auto simp: set_eq_iff intro: top_le le_bot)
+subsection {* Infinite intervals *}
+
+context dense_linorder
+begin
+
+lemma infinite_Ioo:
+ assumes "a < b"
+ shows "\<not> finite {a<..<b}"
+proof
+ assume fin: "finite {a<..<b}"
+ moreover have ne: "{a<..<b} \<noteq> {}"
+ using `a < b` by auto
+ ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"
+ using Max_in[of "{a <..< b}"] by auto
+ then obtain x where "Max {a <..< b} < x" "x < b"
+ using dense[of "Max {a<..<b}" b] by auto
+ then have "x \<in> {a <..< b}"
+ using `a < Max {a <..< b}` by auto
+ then have "x \<le> Max {a <..< b}"
+ using fin by auto
+ with `Max {a <..< b} < x` show False by auto
+qed
+
+lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}"
+ using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]
+ by (auto dest: finite_subset)
+
+lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}"
+ using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]
+ by (auto dest: finite_subset)
+
+lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}"
+ using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]
+ by (auto dest: finite_subset)
+
+end
+
+lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}"
+proof
+ assume "finite {..< a}"
+ then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x"
+ by auto
+ obtain x where "x < a"
+ using lt_ex by auto
+
+ obtain y where "y < Min {..< a}"
+ using lt_ex by auto
+ also have "Min {..< a} \<le> x"
+ using `x < a` by fact
+ also note `x < a`
+ finally have "Min {..< a} \<le> y"
+ by fact
+ with `y < Min {..< a}` show False by auto
+qed
+
+lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}"
+ using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]
+ by (auto simp: subset_eq less_imp_le)
+
+lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}"
+proof
+ assume "finite {a <..}"
+ then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}"
+ by auto
+
+ obtain y where "Max {a <..} < y"
+ using gt_ex by auto
+
+ obtain x where "a < x"
+ using gt_ex by auto
+ also then have "x \<le> Max {a <..}"
+ by fact
+ also note `Max {a <..} < y`
+ finally have "y \<le> Max { a <..}"
+ by fact
+ with `Max {a <..} < y` show False by auto
+qed
+
+lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}"
+ using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]
+ by (auto simp: subset_eq less_imp_le)
+
subsubsection {* Intersection *}
context linorder
@@ -823,6 +910,7 @@
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
+
text{* Any subset of an interval of natural numbers the size of the
subset is exactly that interval. *}
--- a/src/HOL/Topological_Spaces.thy Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Mar 31 21:15:26 2014 +0200
@@ -2134,8 +2134,37 @@
lemma connected_empty[simp]: "connected {}"
by (auto intro!: connectedI)
+lemma connectedD:
+ "connected A \<Longrightarrow> open U \<Longrightarrow> open V \<Longrightarrow> U \<inter> V \<inter> A = {} \<Longrightarrow> A \<subseteq> U \<union> V \<Longrightarrow> U \<inter> A = {} \<or> V \<inter> A = {}"
+ by (auto simp: connected_def)
+
end
+lemma connected_local_const:
+ assumes "connected A" "a \<in> A" "b \<in> A"
+ assumes *: "\<forall>a\<in>A. eventually (\<lambda>b. f a = f b) (at a within A)"
+ shows "f a = f b"
+proof -
+ obtain S where S: "\<And>a. a \<in> A \<Longrightarrow> a \<in> S a" "\<And>a. a \<in> A \<Longrightarrow> open (S a)"
+ "\<And>a x. a \<in> A \<Longrightarrow> x \<in> S a \<Longrightarrow> x \<in> A \<Longrightarrow> f a = f x"
+ using * unfolding eventually_at_topological by metis
+
+ let ?P = "\<Union>b\<in>{b\<in>A. f a = f b}. S b" and ?N = "\<Union>b\<in>{b\<in>A. f a \<noteq> f b}. S b"
+ have "?P \<inter> A = {} \<or> ?N \<inter> A = {}"
+ using `connected A` S `a\<in>A`
+ by (intro connectedD) (auto, metis)
+ then show "f a = f b"
+ proof
+ assume "?N \<inter> A = {}"
+ then have "\<forall>x\<in>A. f a = f x"
+ using S(1) by auto
+ with `b\<in>A` show ?thesis by auto
+ next
+ assume "?P \<inter> A = {}" then show ?thesis
+ using `a \<in> A` S(1)[of a] by auto
+ qed
+qed
+
lemma (in linorder_topology) connectedD_interval:
assumes "connected U" and xy: "x \<in> U" "y \<in> U" and "x \<le> z" "z \<le> y"
shows "z \<in> U"