Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Ceva's Theorem

Email Gateway (Aug 18 2023 at 14:17):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’d like to announce a small new contribution, Ceva's Theorem, by Mathias Schack Rabing

This entry contains a definition of the area the triangle constructed by three points. Building on this, some basic geometric properties about the area of a triangle are derived. These properties are used to prove Ceva's theorem.

[ Which by the way is explained here: https://en.wikipedia.org/wiki/Ceva%27s_theorem ]

You will find it on-line here: https://www.isa-afp.org/entries/Ceva.html

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC