Altitude, Orthocenter of a Triangle and Triangulation

Roland Coghetto

Formalized Mathematics (2016)

  • Volume: 24, Issue: 1, page 27-36
  • ISSN: 1426-2630

Abstract

top
We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.

How to cite

top

Roland Coghetto. "Altitude, Orthocenter of a Triangle and Triangulation." Formalized Mathematics 24.1 (2016): 27-36. <http://eudml.org/doc/286771>.

@article{RolandCoghetto2016,
abstract = {We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {Euclidean geometry; trigonometry; altitude; orthocenter; triangulation; distance},
language = {eng},
number = {1},
pages = {27-36},
title = {Altitude, Orthocenter of a Triangle and Triangulation},
url = {http://eudml.org/doc/286771},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Roland Coghetto
TI - Altitude, Orthocenter of a Triangle and Triangulation
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 1
SP - 27
EP - 36
AB - We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.
LA - eng
KW - Euclidean geometry; trigonometry; altitude; orthocenter; triangulation; distance
UR - http://eudml.org/doc/286771
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] R. Campbell. La trigonométrie. Que sais-je? Presses universitaires de France, 1956. 
  3. [3] Wenpai Chang, Yatsuka Nakamura, and Piotr Rudnicki. Inner products and angles of complex numbers. Formalized Mathematics, 11(3):275-280, 2003. 
  4. [4] Roland Coghetto. Some facts about trigonometry and Euclidean geometry. Formalized Mathematics, 22(4):313-319, 2014. doi:10.2478/forma-2014-0031. Zbl1316.51006
  5. [5] Roland Coghetto. Morley’s trisector theorem. Formalized Mathematics, 23(2):75-79, 2015. doi:10.1515/forma-2015-0007. Zbl1318.51007
  6. [6] Roland Coghetto. Circumcenter, circumcircle and centroid of a triangle. Formalized Mathematics, 24(1):19-29, 2016. doi:10.1515/forma-2016-0002. Zbl1343.51008
  7. [7] H.S.M. Coxeter and S.L. Greitzer. Geometry Revisited. The Mathematical Association of America (Inc.), 1967. Zbl0166.16402
  8. [8] Akihiro Kubo. Lines on planes in n-dimensional Euclidean spaces. Formalized Mathematics, 13(3):389-397, 2005. 
  9. [9] Akihiro Kubo. Lines in n-dimensional Euclidean spaces. Formalized Mathematics, 11(4): 371-376, 2003. 
  10. [10] Akihiro Kubo and Yatsuka Nakamura. Angle and triangle in Euclidean topological space. Formalized Mathematics, 11(3):281-287, 2003. 
  11. [11] Marco Riccardi. Heron’s formula and Ptolemy’s theorem. Formalized Mathematics, 16 (2):97-101, 2008. doi:10.2478/v10037-008-0014-2. 
  12. [12] Boris A. Shminke. Routh’s, Menelaus’ and generalized Ceva’s theorems. Formalized Mathematics, 20(2):157-159, 2012. doi:10.2478/v10037-012-0018-9. Zbl1277.51015
  13. [13] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990. 
  14. [14] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Formalized Mathematics, 7(2):255-263, 1998.  

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.