search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
28 stars 56 forks source link

Add `IsMidpt`? #174

Open jjdishere opened 11 months ago

jjdishere commented 11 months ago

Do we need to follow the custom in Construction folder, write a predicate IsMidpt, instead of (SEG A B).midpoint, the deduce every property of midpoint using hypothesis IsMidpt? Is this necessary?

cybcatppuccino commented 10 months ago

There is no difference between IsMidpt and IsAngleBisector which we have defined. Many problems in geometric exercises use this kind of description.