| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Basic Geometric Properties of Triangles
| Title: | Basic Geometric Properties of Triangles |
| Author: | Manuel Eberl |
| Submission date: | 2015-12-28 |
| Abstract: |
This entry contains a definition of angles between vectors and between three points. Building on this, we prove basic geometric properties of triangles, such as the Isosceles Triangle Theorem, the Law of Sines and the Law of Cosines, that the sum of the angles of a triangle is π, and the congruence theorems for triangles. The definitions and proofs were developed following those by John Harrison in HOL Light. However, due to Isabelle's type class system, all definitions and theorems in the Isabelle formalisation hold for all real inner product spaces. |
| BibTeX: |
@article{Triangle-AFP,
author = {Manuel Eberl},
title = {Basic Geometric Properties of Triangles},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://isa-afp.org/entries/Triangle.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Chord_Segments, Ordinary_Differential_Equations, Stewart_Apollonius |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |