
Basic
Geometric
Properties
of
Triangles
Title: 
Basic Geometric Properties of Triangles 
Author:

Manuel Eberl

Submission date: 
20151228 
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{TriangleAFP,
author = {Manuel Eberl},
title = {Basic Geometric Properties of Triangles},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{https://isaafp.org/entries/Triangle.html},
Formal proof development},
ISSN = {2150914x},
}

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.

