Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

2024-03-01から1ヶ月間の記事一覧

-数学- Lean4のお勉強  3の倍数の確認方法

まだ小学生の頃に習ったことで印象に残っているのは3の倍数の確認方法でした。各桁を足した数が3の倍数ならば元の数も3の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この3の倍数の確認方法の証明を書き下してみようと思いまし…

-数学- Lean4のお勉強 $\sqrt{2}$が無理数であること

Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです…

-数学- Lean4のお勉強 シュレーダー=ベルンシュタインの定理

第4章「集合と関数」の最後のセクションはシュレーダー=ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理:$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, …

-数学- Lean4のお勉強 関数

Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強…