chore(analysis/normed_space/inner_product): notation for orthogonal c…

…omplement (#5536) Notation for `submodule.orthogonal`, so that one can write `Kᗮ` instead of `K.orthogonal`. Simultaneous PR leanprover/vscode-lean#246 adds `\perp` as vscode shorthand for this symbol. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20linear.20algebra.20notation)
leanprover-community · Dec 31, 2020 · 10f6c15 · 10f6c15
1 parent cca6365
commit 10f6c15
Show file tree

Hide file tree

Showing 4 changed files with 74 additions and 77 deletions.
diff --git a/src/analysis/normed_space/dual.lean b/src/analysis/normed_space/dual.lean
@@ -182,9 +182,9 @@ begin
     exact ⟨0, by simp [hℓ]⟩ },
   { have Ycomplete := is_complete_ker ℓ,
     rw [submodule.eq_top_iff_orthogonal_eq_bot Ycomplete, ←hY] at htriv,
-    change Y.orthogonal ≠ ⊥ at htriv,
+    change Yᗮ ≠ ⊥ at htriv,
     rw [submodule.ne_bot_iff] at htriv,
-    obtain ⟨z : E, hz : z ∈ Y.orthogonal, z_ne_0 : z ≠ 0⟩ := htriv,
+    obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv,
     refine ⟨((ℓ z)† / ⟪z, z⟫) • z, _⟩,
     ext x,
     have h₁ : (ℓ z) • x - (ℓ x) • z ∈ Y,

diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
@@ -39,6 +39,8 @@ We globally denote the real and complex inner products by `⟪·, ·⟫_ℝ` and
 We also provide two notation namespaces: `real_inner_product_space`, `complex_inner_product_space`,
 which respectively introduce the plain notation `⟪·, ·⟫` for the the real and complex inner product.
 
+The orthogonal complement of a submodule `K` is denoted by `Kᗮ`.
+
 ## Implementation notes
 
 We choose the convention that inner products are conjugate linear in the first argument and linear
@@ -1634,37 +1636,37 @@ def submodule.orthogonal (K : submodule 𝕜 E) : submodule 𝕜 E :=
   add_mem' := λ x y hx hy u hu, by rw [inner_add_right, hx u hu, hy u hu, add_zero],
   smul_mem' := λ c x hx u hu, by rw [inner_smul_right, hx u hu, mul_zero] }
 
-/-- When a vector is in `K.orthogonal`. -/
-lemma submodule.mem_orthogonal (K : submodule 𝕜 E) (v : E) :
-  v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪u, v⟫ = 0 :=
+notation K`ᗮ`:1200 := submodule.orthogonal K
+
+/-- When a vector is in `Kᗮ`. -/
+lemma submodule.mem_orthogonal (K : submodule 𝕜 E) (v : E) : v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪u, v⟫ = 0 :=
 iff.rfl
 
-/-- When a vector is in `K.orthogonal`, with the inner product the
+/-- When a vector is in `Kᗮ`, with the inner product the
 other way round. -/
-lemma submodule.mem_orthogonal' (K : submodule 𝕜 E) (v : E) :
-  v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪v, u⟫ = 0 :=
+lemma submodule.mem_orthogonal' (K : submodule 𝕜 E) (v : E) : v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫ = 0 :=
 by simp_rw [submodule.mem_orthogonal, inner_eq_zero_sym]
 
-/-- A vector in `K` is orthogonal to one in `K.orthogonal`. -/
+/-- A vector in `K` is orthogonal to one in `Kᗮ`. -/
 lemma submodule.inner_right_of_mem_orthogonal {u v : E} {K : submodule 𝕜 E} (hu : u ∈ K)
-    (hv : v ∈ K.orthogonal) : ⟪u, v⟫ = 0 :=
+    (hv : v ∈ Kᗮ) : ⟪u, v⟫ = 0 :=
 (K.mem_orthogonal v).1 hv u hu
 
-/-- A vector in `K.orthogonal` is orthogonal to one in `K`. -/
+/-- A vector in `Kᗮ` is orthogonal to one in `K`. -/
 lemma submodule.inner_left_of_mem_orthogonal {u v : E} {K : submodule 𝕜 E} (hu : u ∈ K)
-    (hv : v ∈ K.orthogonal) : ⟪v, u⟫ = 0 :=
+    (hv : v ∈ Kᗮ) : ⟪v, u⟫ = 0 :=
 by rw [inner_eq_zero_sym]; exact submodule.inner_right_of_mem_orthogonal hu hv
 
-/-- `K` and `K.orthogonal` have trivial intersection. -/
-lemma submodule.orthogonal_disjoint (K : submodule 𝕜 E) : disjoint K K.orthogonal :=
+/-- `K` and `Kᗮ` have trivial intersection. -/
+lemma submodule.orthogonal_disjoint (K : submodule 𝕜 E) : disjoint K Kᗮ :=
 begin
   simp_rw [submodule.disjoint_def, submodule.mem_orthogonal],
   exact λ x hx ho, inner_self_eq_zero.1 (ho x hx)
 end
 
-/-- `K.orthogonal` can be characterized as the intersection of the kernels of the operations of
+/-- `Kᗮ` can be characterized as the intersection of the kernels of the operations of
 inner product with each of the elements of `K`. -/
-lemma orthogonal_eq_inter (K : submodule 𝕜 E) : K.orthogonal = ⨅ v : K, (inner_right (v:E)).ker :=
+lemma orthogonal_eq_inter (K : submodule 𝕜 E) : Kᗮ = ⨅ v : K, (inner_right (v:E)).ker :=
 begin
   apply le_antisymm,
   { rw le_infi_iff,
@@ -1676,15 +1678,15 @@ begin
 end
 
 /-- The orthogonal complement of any submodule `K` is closed. -/
-lemma submodule.is_closed_orthogonal (K : submodule 𝕜 E) : is_closed (K.orthogonal : set E) :=
+lemma submodule.is_closed_orthogonal (K : submodule 𝕜 E) : is_closed (Kᗮ : set E) :=
 begin
   rw orthogonal_eq_inter K,
   convert is_closed_Inter (λ v : K, (inner_right (v:E)).is_closed_ker),
   simp
 end
 
 /-- In a complete space, the orthogonal complement of any submodule `K` is complete. -/
-instance [complete_space E] (K : submodule 𝕜 E) : complete_space K.orthogonal :=
+instance [complete_space E] (K : submodule 𝕜 E) : complete_space Kᗮ :=
 K.is_closed_orthogonal.complete_space_coe
 
 variables (𝕜 E)
@@ -1701,35 +1703,31 @@ variables {𝕜 E}
 
 /-- `submodule.orthogonal` reverses the `≤` ordering of two
 subspaces. -/
-lemma submodule.orthogonal_le {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
-  K₂.orthogonal ≤ K₁.orthogonal :=
+lemma submodule.orthogonal_le {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) : K₂ᗮ ≤ K₁ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).monotone_l h
 
-/-- `K` is contained in `K.orthogonal.orthogonal`. -/
-lemma submodule.le_orthogonal_orthogonal (K : submodule 𝕜 E) : K ≤ K.orthogonal.orthogonal :=
+/-- `K` is contained in `Kᗮᗮ`. -/
+lemma submodule.le_orthogonal_orthogonal (K : submodule 𝕜 E) : K ≤ Kᗮᗮ :=
 (submodule.orthogonal_gc 𝕜 E).le_u_l _
 
 /-- The inf of two orthogonal subspaces equals the subspace orthogonal
 to the sup. -/
-lemma submodule.inf_orthogonal (K₁ K₂ : submodule 𝕜 E) :
-  K₁.orthogonal ⊓ K₂.orthogonal = (K₁ ⊔ K₂).orthogonal :=
+lemma submodule.inf_orthogonal (K₁ K₂ : submodule 𝕜 E) : K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).l_sup.symm
 
 /-- The inf of an indexed family of orthogonal subspaces equals the
 subspace orthogonal to the sup. -/
-lemma submodule.infi_orthogonal {ι : Type*} (K : ι → submodule 𝕜 E) :
-  (⨅ i, (K i).orthogonal) = (supr K).orthogonal :=
+lemma submodule.infi_orthogonal {ι : Type*} (K : ι → submodule 𝕜 E) : (⨅ i, (K i)ᗮ) = (supr K)ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).l_supr.symm
 
 /-- The inf of a set of orthogonal subspaces equals the subspace
 orthogonal to the sup. -/
-lemma submodule.Inf_orthogonal (s : set $ submodule 𝕜 E) :
-  (⨅ K ∈ s, submodule.orthogonal K) = (Sup s).orthogonal :=
+lemma submodule.Inf_orthogonal (s : set $ submodule 𝕜 E) : (⨅ K ∈ s, Kᗮ) = (Sup s)ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).l_Sup.symm
 
-/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁.orthogonal ⊓ K₂` span `K₂`. -/
+/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁ᗮ ⊓ K₂` span `K₂`. -/
 lemma submodule.sup_orthogonal_inf_of_is_complete {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂)
-  (hc : is_complete (K₁ : set E)) : K₁ ⊔ (K₁.orthogonal ⊓ K₂) = K₂ :=
+  (hc : is_complete (K₁ : set E)) : K₁ ⊔ (K₁ᗮ ⊓ K₂) = K₂ :=
 begin
   ext x,
   rw submodule.mem_sup,
@@ -1742,34 +1740,33 @@ begin
                  add_sub_cancel'_right _ _⟩ }
 end
 
-/-- If `K` is complete, `K` and `K.orthogonal` span the whole
+/-- If `K` is complete, `K` and `Kᗮ` span the whole
 space. -/
 lemma submodule.sup_orthogonal_of_is_complete {K : submodule 𝕜 E} (h : is_complete (K : set E)) :
-  K ⊔ K.orthogonal = ⊤ :=
+  K ⊔ Kᗮ = ⊤ :=
 begin
   convert submodule.sup_orthogonal_inf_of_is_complete (le_top : K ≤ ⊤) h,
   simp
 end
 
-/-- If `K` is complete, `K` and `K.orthogonal` span the whole space. Version using `complete_space`.
+/-- If `K` is complete, `K` and `Kᗮ` span the whole space. Version using `complete_space`.
 -/
 lemma submodule.sup_orthogonal_of_complete_space {K : submodule 𝕜 E} [complete_space K] :
-  K ⊔ K.orthogonal = ⊤ :=
+  K ⊔ Kᗮ = ⊤ :=
 submodule.sup_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›)
 
 /-- If `K` is complete, any `v` in `E` can be expressed as a sum of elements of `K` and
-`K.orthogonal`. -/
+`Kᗮ`. -/
 lemma submodule.exists_sum_mem_mem_orthogonal (K : submodule 𝕜 E) [complete_space K] (v : E) :
-  ∃ (y ∈ K) (z ∈ K.orthogonal), v = y + z :=
+  ∃ (y ∈ K) (z ∈ Kᗮ), v = y + z :=
 begin
-  have h_mem : v ∈ K ⊔ K.orthogonal := by simp [submodule.sup_orthogonal_of_complete_space],
+  have h_mem : v ∈ K ⊔ Kᗮ := by simp [submodule.sup_orthogonal_of_complete_space],
   obtain ⟨y, hy, z, hz, hyz⟩ := submodule.mem_sup.mp h_mem,
   exact ⟨y, hy, z, hz, hyz.symm⟩
 end
 
 /-- If `K` is complete, then the orthogonal complement of its orthogonal complement is itself. -/
-@[simp] lemma submodule.orthogonal_orthogonal (K : submodule 𝕜 E) [complete_space K] :
-  K.orthogonal.orthogonal = K :=
+@[simp] lemma submodule.orthogonal_orthogonal (K : submodule 𝕜 E) [complete_space K] : Kᗮᗮ = K :=
 begin
   ext v,
   split,
@@ -1784,31 +1781,31 @@ begin
     exact hw v hv }
 end
 
-/-- If `K` is complete, `K` and `K.orthogonal` are complements of each
+/-- If `K` is complete, `K` and `Kᗮ` are complements of each
 other. -/
 lemma submodule.is_compl_orthogonal_of_is_complete {K : submodule 𝕜 E}
-    (h : is_complete (K : set E)) : is_compl K K.orthogonal :=
+  (h : is_complete (K : set E)) : is_compl K Kᗮ :=
 ⟨K.orthogonal_disjoint, le_of_eq (submodule.sup_orthogonal_of_is_complete h).symm⟩
 
-@[simp] lemma submodule.top_orthogonal_eq_bot : (⊤ : submodule 𝕜 E).orthogonal = ⊥ :=
+@[simp] lemma submodule.top_orthogonal_eq_bot : (⊤ : submodule 𝕜 E)ᗮ = ⊥ :=
 begin
   ext,
   rw [submodule.mem_bot, submodule.mem_orthogonal],
   exact ⟨λ h, inner_self_eq_zero.mp (h x submodule.mem_top), by { rintro rfl, simp }⟩
 end
 
-@[simp] lemma submodule.bot_orthogonal_eq_top : (⊥ : submodule 𝕜 E).orthogonal = ⊤ :=
+@[simp] lemma submodule.bot_orthogonal_eq_top : (⊥ : submodule 𝕜 E)ᗮ = ⊤ :=
 begin
   rw [← submodule.top_orthogonal_eq_bot, eq_top_iff],
   exact submodule.le_orthogonal_orthogonal ⊤
 end
 
 lemma submodule.eq_top_iff_orthogonal_eq_bot {K : submodule 𝕜 E} (hK : is_complete (K : set E)) :
-  K = ⊤ ↔ K.orthogonal = ⊥ :=
+  K = ⊤ ↔ Kᗮ = ⊥ :=
 begin
   refine ⟨by { rintro rfl, exact submodule.top_orthogonal_eq_bot }, _⟩,
   intro h,
-  have : K ⊔ K.orthogonal = ⊤ := submodule.sup_orthogonal_of_is_complete hK,
+  have : K ⊔ Kᗮ = ⊤ := submodule.sup_orthogonal_of_is_complete hK,
   rwa [h, sup_comm, bot_sup_eq] at this,
 end
 
@@ -1819,10 +1816,10 @@ containined in it, the dimensions of `K₁` and the intersection of its
 orthogonal subspace with `K₂` add to that of `K₂`. -/
 lemma submodule.findim_add_inf_findim_orthogonal {K₁ K₂ : submodule 𝕜 E}
   [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) :
-  findim 𝕜 K₁ + findim 𝕜 (K₁.orthogonal ⊓ K₂ : submodule 𝕜 E) = findim 𝕜 K₂ :=
+  findim 𝕜 K₁ + findim 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = findim 𝕜 K₂ :=
 begin
   haveI := submodule.finite_dimensional_of_le h,
-  have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁.orthogonal ⊓ K₂),
+  have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁ᗮ ⊓ K₂),
   rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, findim_bot,
       submodule.sup_orthogonal_inf_of_is_complete h
         (submodule.complete_of_finite_dimensional _)] at hd,

diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
@@ -545,10 +545,10 @@ def orthogonal_projection_fn (s : affine_subspace ℝ P) [nonempty s] [complete_
   (p : P) : P :=
 classical.some $ inter_eq_singleton_of_nonempty_of_is_compl
   (nonempty_subtype.mp ‹_›)
-  (mk'_nonempty p s.direction.orthogonal)
+  (mk'_nonempty p s.directionᗮ)
   begin
     convert submodule.is_compl_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›),
-    exact direction_mk' p s.direction.orthogonal
+    exact direction_mk' p s.directionᗮ
   end
 
 /-- The intersection of the subspace and the orthogonal subspace
@@ -558,13 +558,13 @@ setting up the bundled version and should not be used once that is
 defined. -/
 lemma inter_eq_singleton_orthogonal_projection_fn {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] (p : P) :
-  (s : set P) ∩ (mk' p s.direction.orthogonal) = {orthogonal_projection_fn s p} :=
+  (s : set P) ∩ (mk' p s.directionᗮ) = {orthogonal_projection_fn s p} :=
 classical.some_spec $ inter_eq_singleton_of_nonempty_of_is_compl
   (nonempty_subtype.mp ‹_›)
-  (mk'_nonempty p s.direction.orthogonal)
+  (mk'_nonempty p s.directionᗮ)
   begin
     convert submodule.is_compl_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›),
-    exact direction_mk' p s.direction.orthogonal
+    exact direction_mk' p s.directionᗮ
   end
 
 /-- The `orthogonal_projection_fn` lies in the given subspace.  This
@@ -582,7 +582,7 @@ subspace.  This lemma is only intended for use in setting up the
 bundled version and should not be used once that is defined. -/
 lemma orthogonal_projection_fn_mem_orthogonal {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] (p : P) :
-  orthogonal_projection_fn s p ∈ mk' p s.direction.orthogonal :=
+  orthogonal_projection_fn s p ∈ mk' p s.directionᗮ :=
 begin
   rw [←mem_coe, ←set.singleton_subset_iff, ←inter_eq_singleton_orthogonal_projection_fn],
   exact set.inter_subset_right _ _
@@ -594,8 +594,8 @@ use in setting up the bundled version and should not be used once that
 is defined. -/
 lemma orthogonal_projection_fn_vsub_mem_direction_orthogonal {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] (p : P) :
-  orthogonal_projection_fn s p -ᵥ p ∈ s.direction.orthogonal :=
-direction_mk' p s.direction.orthogonal ▸
+  orthogonal_projection_fn s p -ᵥ p ∈ s.directionᗮ :=
+direction_mk' p s.directionᗮ ▸
   vsub_mem_direction (orthogonal_projection_fn_mem_orthogonal p) (self_mem_mk' _ _)
 
 /-- The orthogonal projection of a point onto a nonempty affine
@@ -613,7 +613,7 @@ def orthogonal_projection (s : affine_subspace ℝ P) [nonempty s] [complete_spa
       vadd_mem_of_mem_direction (orthogonal_projection s.direction v).2
                                 (orthogonal_projection_fn_mem p),
     have ho : ((orthogonal_projection s.direction) v : V) +ᵥ orthogonal_projection_fn s p ∈
-      mk' (v +ᵥ p) s.direction.orthogonal,
+      mk' (v +ᵥ p) s.directionᗮ,
     { rw [←vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk',
           vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc],
       refine submodule.add_mem _ (orthogonal_projection_fn_vsub_mem_direction_orthogonal p) _,
@@ -645,7 +645,7 @@ through the given point is the `orthogonal_projection` of that point
 onto the subspace. -/
 lemma inter_eq_singleton_orthogonal_projection {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] (p : P) :
-  (s : set P) ∩ (mk' p s.direction.orthogonal) = {orthogonal_projection s p} :=
+  (s : set P) ∩ (mk' p s.directionᗮ) = {orthogonal_projection s p} :=
 begin
   rw ←orthogonal_projection_fn_eq,
   exact inter_eq_singleton_orthogonal_projection_fn p
@@ -659,7 +659,7 @@ lemma orthogonal_projection_mem {s : affine_subspace ℝ P} [nonempty s] [comple
 /-- The `orthogonal_projection` lies in the orthogonal subspace. -/
 lemma orthogonal_projection_mem_orthogonal (s : affine_subspace ℝ P) [nonempty s]
   [complete_space s.direction] (p : P) :
-  ↑(orthogonal_projection s p) ∈ mk' p s.direction.orthogonal :=
+  ↑(orthogonal_projection s p) ∈ mk' p s.directionᗮ :=
 orthogonal_projection_fn_mem_orthogonal p
 
 /-- Subtracting a point in the given subspace from the
@@ -686,7 +686,7 @@ begin
   split,
   { exact λ h, h ▸ orthogonal_projection_mem p },
   { intro h,
-    have hp : p ∈ ((s : set P) ∩ mk' p s.direction.orthogonal) := ⟨h, self_mem_mk' p _⟩,
+    have hp : p ∈ ((s : set P) ∩ mk' p s.directionᗮ) := ⟨h, self_mem_mk' p _⟩,
     rw [inter_eq_singleton_orthogonal_projection p] at hp,
     symmetry,
     exact hp }
@@ -728,23 +728,23 @@ mt dist_orthogonal_projection_eq_zero_iff.mp hp
 in the orthogonal direction. -/
 lemma orthogonal_projection_vsub_mem_direction_orthogonal (s : affine_subspace ℝ P) [nonempty s]
   [complete_space s.direction] (p : P) :
-  (orthogonal_projection s p : P) -ᵥ p ∈ s.direction.orthogonal :=
+  (orthogonal_projection s p : P) -ᵥ p ∈ s.directionᗮ :=
 orthogonal_projection_fn_vsub_mem_direction_orthogonal p
 
 /-- Subtracting the `orthogonal_projection` from `p` produces a result
 in the orthogonal direction. -/
 lemma vsub_orthogonal_projection_mem_direction_orthogonal (s : affine_subspace ℝ P) [nonempty s]
   [complete_space s.direction] (p : P) :
-  p -ᵥ orthogonal_projection s p ∈ s.direction.orthogonal :=
-direction_mk' p s.direction.orthogonal ▸
+  p -ᵥ orthogonal_projection s p ∈ s.directionᗮ :=
+direction_mk' p s.directionᗮ ▸
   vsub_mem_direction (self_mem_mk' _ _) (orthogonal_projection_mem_orthogonal s p)
 
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector was
 in the orthogonal direction. -/
 lemma orthogonal_projection_vadd_eq_self {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] {p : P} (hp : p ∈ s) {v : V}
-  (hv : v ∈ s.direction.orthogonal) :
+  (hv : v ∈ s.directionᗮ) :
   orthogonal_projection s (v +ᵥ p) = ⟨p, hp⟩ :=
 begin
   have h := vsub_orthogonal_projection_mem_direction_orthogonal s (v +ᵥ p),
@@ -788,7 +788,7 @@ adding multiples of the same orthogonal vector to points in the same
 subspace. -/
 lemma dist_square_smul_orthogonal_vadd_smul_orthogonal_vadd {s : affine_subspace ℝ P}
     {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) (r1 r2 : ℝ) {v : V}
-    (hv : v ∈ s.direction.orthogonal) :
+    (hv : v ∈ s.directionᗮ) :
   dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) =
     dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (∥v∥ * ∥v∥) :=
 calc dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2)
@@ -944,7 +944,7 @@ end
 produces the negation of that vector plus the point. -/
 lemma reflection_orthogonal_vadd {s : affine_subspace ℝ P} [nonempty s]
   [complete_space s.direction] {p : P} (hp : p ∈ s) {v : V}
-  (hv : v ∈ s.direction.orthogonal) : reflection s (v +ᵥ p) = -v +ᵥ p :=
+  (hv : v ∈ s.directionᗮ) : reflection s (v +ᵥ p) = -v +ᵥ p :=
 begin
   rw [reflection_apply, orthogonal_projection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub],
   simp