| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Stewart's Theorem and Apollonius' Theorem
| Title: | Stewart's Theorem and Apollonius' Theorem |
| Author: | Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com) |
| Submission date: | 2017-07-31 |
| Abstract: | This entry formalizes the two geometric theorems, Stewart's and Apollonius' theorem. Stewart's Theorem relates the length of a triangle's cevian to the lengths of the triangle's two sides. Apollonius' Theorem is a specialisation of Stewart's theorem, restricting the cevian to be the median. The proof applies the law of cosines, some basic geometric facts about triangles and then simply transforms the terms algebraically to yield the conjectured relation. The formalization in Isabelle can closely follow the informal proofs described in the Wikipedia articles of those two theorems. |
| BibTeX: |
@article{Stewart_Apollonius-AFP,
author = {Lukas Bulwahn},
title = {Stewart's Theorem and Apollonius' Theorem},
journal = {Archive of Formal Proofs},
month = jul,
year = 2017,
note = {\url{https://isa-afp.org/entries/Stewart_Apollonius.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Triangle |
| 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 |