--- a/src/HOL/Real_Vector_Spaces.thy Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Feb 07 14:10:08 2023 +0000
@@ -986,6 +986,9 @@
for a b :: "'a::{real_normed_field,field}"
by (simp add: divide_inverse norm_mult norm_inverse)
+lemma dist_divide_right: "dist (a/c) (b/c) = dist a b / norm c" for c :: "'a :: real_normed_field"
+ by (metis diff_divide_distrib dist_norm norm_divide)
+
lemma norm_inverse_le_norm:
fixes x :: "'a::real_normed_div_algebra"
shows "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
@@ -1134,7 +1137,6 @@
finally show ?thesis .
qed
-
subsection \<open>Metric spaces\<close>
class metric_space = uniformity_dist + open_uniformity +