--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Apr 07 21:05:22 2019 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Apr 08 15:26:54 2019 +0100
@@ -34,6 +34,9 @@
subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
+lemma orthogonal_Basis: "pairwise orthogonal Basis"
+ by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
+
lemma representation_bound:
fixes B :: "'N::real_inner set"
assumes "finite B" "independent B" "b \<in> B" and orth: "pairwise orthogonal B"