Heron's Formula and Ptolemy's Theorem

Marco Riccardi

Formalized Mathematics (2008)

  • Volume: 16, Issue: 2, page 97-101
  • ISSN: 1426-2630

Abstract

top
The goal of this article is to formalize some theorems that are in the [17] on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.MML identifier: EUCLID 6, version: 7.8.09 4.97.1001

How to cite

top

Marco Riccardi. "Heron's Formula and Ptolemy's Theorem." Formalized Mathematics 16.2 (2008): 97-101. <http://eudml.org/doc/267235>.

@article{MarcoRiccardi2008,
abstract = {The goal of this article is to formalize some theorems that are in the [17] on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.MML identifier: EUCLID 6, version: 7.8.09 4.97.1001},
author = {Marco Riccardi},
journal = {Formalized Mathematics},
language = {eng},
number = {2},
pages = {97-101},
title = {Heron's Formula and Ptolemy's Theorem},
url = {http://eudml.org/doc/267235},
volume = {16},
year = {2008},
}

TY - JOUR
AU - Marco Riccardi
TI - Heron's Formula and Ptolemy's Theorem
JO - Formalized Mathematics
PY - 2008
VL - 16
IS - 2
SP - 97
EP - 101
AB - The goal of this article is to formalize some theorems that are in the [17] on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.MML identifier: EUCLID 6, version: 7.8.09 4.97.1001
LA - eng
UR - http://eudml.org/doc/267235
ER -

References

top
  1. [1] Kanchun and Yatsuka Nakamura. The inner product of finite sequences and of points of n-dimensional topological space. Formalized Mathematics, 11(2):179-183, 2003. 
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991. 
  4. [4] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  5. [5] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  6. [6] Wenpai Chang, Yatsuka Nakamura, and Piotr Rudnicki. Inner products and angles of complex numbers. Formalized Mathematics, 11(3):275-280, 2003. 
  7. [7] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991. 
  8. [8] Agata Darmochwał and Yatsuka Nakamura. The topological space ε2/T. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617-621, 1991. 
  9. [9] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990. 
  10. [10] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990. 
  11. [11] Akihiro Kubo and Yatsuka Nakamura. Angle and triangle in Euclidian topological space. Formalized Mathematics, 11(3):281-287, 2003. 
  12. [12] Yatsuka Nakamura. General Fashoda meet theorem for unit circle and square. Formalized Mathematics, 11(3):213-224, 2003. 
  13. [13] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  14. [14] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990. 
  15. [15] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  16. [16] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  17. [17] Freek Wiedijk. Formalizing 100 theorems. 
  18. [18] 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.