3段階で考えよう
- f ≠ 0という否定は、f = 0の証拠があればFalseという矛盾を得ること。
- 両方が同じ空間の、まさに同じ対象についての主張である必要があります。別々の形式なら性質が違っても構いません。
- 非零の証拠にゼロの証拠を適用すると、不可能な枝を閉じ、出発点の仮定を排除できます。
小さな例で確かめる
一つのfについてf ≠ 0とf = 0は両立しません。非零のfと、別のゼロのgなら矛盾ではありません。
順番 63 / 64
高校
同じ対象についての矛盾
同じfについて、f ≠ 0とf = 0の証拠は両立しません。
まず、身近な例で
「この箱のあめは0個」と「この同じ箱のあめは0個ではない」は、同時には成り立ちません。別々の箱なら矛盾しません。同じ対象を比べることが大切です。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
別々の箱なら、中の量が違っても構いません。同じ対象・同じ条件について、両立しない主張があるかを見ます。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、別の対象なら両立する。 別々の箱なら、中の量が違っても構いません。同じ対象・同じ条件について、両立しない主張があるかを見ます。
Leanでの使用例・原文の抜粋
FLT · aa2d8b3 · S_FreyPackage_no_frey_package.lean
hf (ModularForm.S2_Gamma0_2_eq_zero f)このLeanの読み方
hfは非零の証拠。そこへ渡す引数が同じ形式のゼロを示します。これは矛盾を得る適用で、新しい公理ではありません。