3段階で考えよう
- まず対象を読む。(a : ℕ)は「aは自然数」。ℕには0が入り、ℤには負の整数も入ります。
- 条件も一つの主張です。ha : 0 < aは「aが正」の証拠にhaという名前を付けたもの。Propは主張の型です。
- ∀は「すべて」、∃は「ある」、∧は「かつ」、→は「ならば」。structureは対象と、その条件の証拠をまとめる仕組みです。
小さな例で確かめる
小包のa : ℤは数、ha0 : a ≠ 0はその数が0ではないという証拠です。
順番 1 / 64
高校
Leanの主張を読む
対象・条件・結論を分けて読みます。
まず、身近な例で
「正の整数を選んで」と言われたら、0や負の数は入れられません。nを動かしてn > 0が成り立つか見よう。条件は名前の飾りではなく、確かめることです。
n = 1：1 > 0 ✓
この例と、本当の定義の違い
ここで確かめるのは一つの数の条件で、Leanの証明や、この章の仮定全体ではありません。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
0は整数ですが、正ではありません。数の種類と、追加の条件は別々に確かめます。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ。 0は整数ですが、正ではありません。数の種類と、追加の条件は別々に確かめます。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean
structure FreyPackage wherea : ℤb : ℤc : ℤha0 : a ≠ 0hb0 : b ≠ 0hc0 : c ≠ 0p : ℕpp : Nat.Prime php5 : 5 ≤ phFLT : a ^ p + b ^ p = c ^ phgcdab : gcd a b = 1ha4 : (a : ZMod 4) = 3
このLeanの読み方
a・b・cのデータ欄を先に、その後でha0・hb0・hc0の証拠欄を読みます。欄の名前そのものは新しい数学用語ではありません。