--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Nov 04 17:59:32 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Nov 04 19:53:43 2019 -0500
@@ -179,11 +179,21 @@
shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps mem_cball)
+lemma cball_eq_atLeastAtMost:
+ fixes a b::real
+ shows "cball a b = {a - b .. a + b}"
+ by (auto simp: dist_real_def)
+
lemma greaterThanLessThan_eq_ball:
fixes a b::real
shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps mem_ball)
+lemma ball_eq_greaterThanLessThan:
+ fixes a b::real
+ shows "ball a b = {a - b <..< a + b}"
+ by (auto simp: dist_real_def)
+
lemma interior_ball [simp]: "interior (ball x e) = ball x e"
by (simp add: interior_open)