search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
27 stars 56 forks source link

Directed Line #156

Open jjdishere opened 1 year ago

jjdishere commented 1 year ago

A concept very useful in Position, and is easy to use in LCPosition.

It is a quotient of Ray and Line is a quotient of it.

jjdishere commented 12 months ago

directed line need a lot of coersion lemmas, angle can be mk from directed line, 内错角 同旁内角 is easy to formulate using directed line.

jjdishere commented 12 months ago

Only definition DirLine is written now. All properties waiting to be added