--- a/src/HOL/Analysis/Connected.thy Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Mon Feb 26 07:34:05 2018 +0100
@@ -2727,6 +2727,13 @@
using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
by auto
+lemma bounded_two_points:
+ "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"
+ apply (rule iffI)
+ subgoal using diameter_bounded(1) by auto
+ subgoal using bounded_any_center[of S] by meson
+ done
+
lemma diameter_compact_attained:
assumes "compact s"
and "s \<noteq> {}"
@@ -3797,6 +3804,14 @@
using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
+text \<open>Connectedness is invariant under homeomorphisms.\<close>
+
+lemma homeomorphic_connectedness:
+ assumes "s homeomorphic t"
+ shows "connected s \<longleftrightarrow> connected t"
+using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
+
+
subsection\<open>Inverse function property for open/closed maps\<close>
lemma continuous_on_inverse_open_map: