lean4

まずは数列の極限の証明を見て見ましょう。 $$\lim_{n\to\infty}n = \infty\hspace{20cm}$$ example : Tendsto (fun n:ℕ => n) atTop atTop := by exact tendsto_id exact一発で終わるということは全く同じか、より一般化された証明があるということです。この場合は少し一般化された定理tendsto_idがすでにmathlib4にあり、それが使われました。 tendsto_idという定理はFilter.tendsto_id.{u_1} {α : Type u_1} {x : Filter α} …

Mathematics in Lean 4も最後の方に辿り着きつつあります。これから数回にわたってLean4による解析学の証明を見ていきます。Mathematics In Lean 4の章立てで言えば10.1 Filtersあたりなのですが、そこでの扱いはもっとはるかに抽象的です。この記事では具体例を中心に説明します。 まずは極限ですよね。普通の数学では$\varepsilon - \delta$論法が証明の中心です。一方Lean 4では定義域や値域での極限操作をフィルタという概念で統一的に表現しています。フィルタの概念のレベルで証明が完結する場合もあれば、それを不等式や集合に展開して個別のケ…

前回の記事 -数学- Lean4のお勉強 ラグランジュの定理の続き - Maxima で綴る数学の旅 は色々と修正するべき点や補おう点があり、ここに書き直すことにしました。 前回はGを群、G'をその部分群としてG ≃ (G ⧸ G') × G'という定理の証明について解説しようとしました。まずはこの定理の意味の理解が間違っていたのでそこから始めます。前回の記事では≃は群同型を表すと書きましたが、これは集合の同型でした。つまり、Gと(G ⧸ G') × G'の間には双射がある、すなわちGから(G ⧸ G') × G'への写像toFunと(G ⧸ G') × G'からGへの写像invFunがあり、…

今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。 8.1.3のハイライトはラグランジュの定理です。 ラグランジュの定理：有限群の部分群の位数はもとの群の位数の約数である。 |G|=[G:G'] |G'| 、あるいは同じことだが、|G|=|G/G'| |G'| ここにGはある有限群、G'はその部分群、| |は群の位数（集合の要素数）、[G:G']はGにおけるG'の指数、G/G'はG'によるGの左剰余類の集合。 多分高校生の頃にこの定理は知っていたと思うのですが、腹落ちして感動したのは大学に入ってからだったと思います。抽象的な代数構造に見える…

Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。 ここまでくれば環を定義することができます。 class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where /-- Multiplication is left distributive over addition -/ left_distrib : ∀ a b c : R, a *…

Mathematics In Leanから第7章 階層 7.1 基礎の勉強を続けます。 "At this stage we would like to move on to define rings"というあたりで、ここから環を定義していきます。 環を定義するにあたっての課題意識は環の２つの演算である加法群と乗法モノイドでは全ての乗法モノイドの定理は加法群でも成り立つことです。この部分を自動的に行う仕組みが必要になります。 使う道具立てはAdd, AddZero, Mul, MulOne, Neg, InvというLean標準定義済みのクラスです。ちなみに明示的には登場しませんが、これらのクラス…

群にあってモノイドにないものは、、、そう、逆元です。モノイドにはすでに演算があり単位元があり演算は結合的でした。そこに全ての元に逆元があれば群になるわけです。 一旦前回までに定義した道具立てを再掲しておきます。 class Semigroup₂ (α : Type) extends Dia₁ α where /-- Diamond is associative -/ dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c) class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where /-- One…