# 直角三角形

具有一個內角為直角的三角形。

mko-right-triangle · definition · v0.5.0



## 數學敘述

若三角形的一個內角等於九十度，或以弧度表示為 π/2，則此三角形稱為直角三角形。





## 代表公式（精確 TeX）

\gamma=\frac{\pi}{2}





## 成立條件


- 討論對象是平面中的非退化三角形。
- 角度使用度數或弧度表示，且 90° 與 π/2 表示同一角度。





## 符號作用域


- γ — 被指定為直角的內角
- π — 圓周率





## 直觀、定義與常見誤解

三角形最多只能有一個直角，因為三個內角的總和為 180°。

直角所對的邊稱為斜邊，另外兩邊稱為股；斜邊是三邊中最長的一邊。

程式可以檢查三個輸入角是否在容差內加總為 180°，並判斷其中是否存在 90°；這仍只是對具體輸入的檢查。

只看到某兩條邊互相垂直，卻沒有確認它們與第三邊構成非退化三角形。





## 已採用的推導導讀

[直角三角形：用座標判定哪一個內角是直角](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-right-triangle-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識







## 驗證界線

有限角度案例通過只表示參考程式符合所列測試，不等於完成幾何定義的形式化。

not_formalized


- [evidence-sha256-d2f7e95c5eb44099070a59498f1ad1b82c0818327df33683b6e82d8624544ea9](https://ocme.evemisslab.com/data/evidence/d2f7e95c5eb44099070a59498f1ad1b82c0818327df33683b6e82d8624544ea9.json)





## 下一個義務

對接 Mathlib 的三角形、角度與垂直關係定義。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/right-triangle.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-right-triangle/index.md)