Add type annotation

avigad · Sep 19, 2023 · 92821f6 · 92821f6
1 parent 376631a
commit 92821f6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C08_Topology/S02_Metric_Spaces.lean b/MIL/C08_Topology/S02_Metric_Spaces.lean
@@ -432,7 +432,7 @@ theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
     dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
     _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
     _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
-    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry
+    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
     _ ≤ 1 / 2 ^ N * 2 := sorry
     _ < ε := sorry