Skip to content

Commit

Permalink
Update Euclidean.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
Vtec234 authored Sep 25, 2024
1 parent a08c9f9 commit f152c32
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ProofWidgets/Demos/Euclidean.lean
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ and not in the diagram.
- To construct a circle with center `a` passing through `b`,
select `a` and `b` in `a b : Point`.
You may have to prove that `a ≠ b`.
- To construct an interesection point of two circles `C` and `D`,
- To construct an intersection point of two circles `C` and `D`,
you first have to provide a local proof
of `have h : circlesInter C D := ...`
(i.e., show that the circles intersect)
Expand Down

0 comments on commit f152c32

Please sign in to comment.