Skip to content

Commit c55817d

Browse files
authored
fix(pitfalls.md): remove repeated word (#760)
In [pitfalls.md / Distance in Fin n → ℝ](https://leanprover-community.github.io/extras/pitfalls.html#distance-in-fin-n--%E2%84%9D), in the sentence > To instead use the standard Euclidean metric (also called the $L^2$ metric), you must use instead use `EuclideanSpace ℝ (Fin n)` I removed the double "use" and the double "instead".
1 parent 3ba32ed commit c55817d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

templates/extras/pitfalls.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -453,7 +453,7 @@ example : dist ![(1 : ℝ),0] ![0,1] = 1 := by
453453
fin_cases b <;> simp
454454
```
455455

456-
To instead use the standard Euclidean metric (also called the $L^2$ metric), you must use instead use `EuclideanSpace ℝ (Fin n)`, which is an abbreviation for `WithLp 2 (Fin n → ℝ)`. Vectors of this type can be written using the `!₂[x,y,z,...]` notation.
456+
To instead use the standard Euclidean metric (also called the $L^2$ metric), you must use `EuclideanSpace ℝ (Fin n)`, which is an abbreviation for `WithLp 2 (Fin n → ℝ)`. Vectors of this type can be written using the `!₂[x,y,z,...]` notation.
457457
```lean
458458
example : dist !₂[(1 : ℝ),0] !₂[0,1] = √2 := by
459459
norm_num [EuclideanSpace.dist_eq]

0 commit comments

Comments
 (0)