We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents a43321f + 3c4593c commit 6adbae9Copy full SHA for 6adbae9
lean4/src/putnam_1996_a2.lean
@@ -13,5 +13,5 @@ theorem putnam_1996_a2
13
(hC1 : C1 = sphere O1 1)
14
(hC2 : C2 = sphere O2 3)
15
(hO1O2 : dist O1 O2 = 10)
16
-: {M : EuclideanSpace ℝ (Fin 2) | ∃ X Y : Fin 2 → ℝ, X ∈ C1 ∧ Y ∈ C2 ∧ M = midpoint ℝ X Y} = putnam_1996_a2_solution O1 O2 :=
+: {M : EuclideanSpace ℝ (Fin 2) | ∃ X Y, X ∈ C1 ∧ Y ∈ C2 ∧ M = midpoint ℝ X Y} = putnam_1996_a2_solution O1 O2 :=
17
sorry
0 commit comments