Circumcenter, Circumcircle and Centroid of a Triangle

Roland Coghetto

Formalized Mathematics (2016)

  • Volume: 24, Issue: 1, page 17-26
  • ISSN: 1426-2630

Abstract

top
We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.

How to cite

top

Roland Coghetto. "Circumcenter, Circumcircle and Centroid of a Triangle." Formalized Mathematics 24.1 (2016): 17-26. <http://eudml.org/doc/286770>.

@article{RolandCoghetto2016,
abstract = {We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {Euclidean geometry; perpendicular bisector; circumcenter; circumcircle; centroid; extended law of sines},
language = {eng},
number = {1},
pages = {17-26},
title = {Circumcenter, Circumcircle and Centroid of a Triangle},
url = {http://eudml.org/doc/286770},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Roland Coghetto
TI - Circumcenter, Circumcircle and Centroid of a Triangle
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 1
SP - 17
EP - 26
AB - We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.
LA - eng
KW - Euclidean geometry; perpendicular bisector; circumcenter; circumcircle; centroid; extended law of sines
UR - http://eudml.org/doc/286770
ER -

References

top
  1. [1] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17. Zbl06512423
  2. [2] Czesław Byliński. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99-107, 2005. 
  3. [3] H.S.M. Coxeter and S.L. Greitzer. Geometry Revisited. The Mathematical Association of America (Inc.), 1967. Zbl0166.16402
  4. [4] Robin Hartshorne. Geometry: Euclid and beyond. Springer, 2000. 
  5. [5] Akihiro Kubo. Lines on planes in n-dimensional Euclidean spaces. Formalized Mathematics, 13(3):389-397, 2005. 
  6. [6] Marco Riccardi. Heron’s formula and Ptolemy’s theorem. Formalized Mathematics, 16(2): 97-101, 2008. doi:10.2478/v10037-008-0014-2. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.