数学 › 数理論理学と型理論 › 証明支援系 Lean の仕組み

Lean の公理

公理 6.1（「証明支援系 Lean の仕組み」§6）

  1. 命題外延性 propext：同値な命題は等しい。
  2. 商の健全性 Quot.sound：r a br\,a\,b ならば、商 Quot r で aa と bb の類は等しい。
  3. 大域選択 Classical.choice：型 α\alpha が空でない（Nonempty α。これは Prop に属する）ならば、α\alpha の元を一つ返す。

本文で読む（前後の説明と例）→

閉包の状態

公理

公理は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 2 問