diff --git a/MIL/C01_Introduction/S01_Getting_Started.lean b/MIL/C01_Introduction/S01_Getting_Started.lean index 4e45fe6e..bda30f7e 100644 --- a/MIL/C01_Introduction/S01_Getting_Started.lean +++ b/MIL/C01_Introduction/S01_Getting_Started.lean @@ -101,9 +101,9 @@ OMIT. -/ 1. ``ctrl+shift+P`` (Macの場合は ``command+shift+P`` )を押します． -2. 上記手順で現れたバーで ``Lean 4: Open Documentation View`` と打ち込み，エンターキーを押します．（もしくはメニュー内で上記の文字列が選択されてハイライトされている場合はそのままエンターキーを押しても良いです．） +2. 上記手順で現れたバーで ``Lean 4: Docs: Show Documentation Resources`` と打ち込み，エンターキーを押します．（もしくはメニュー内で上記の文字列が選択されてハイライトされている場合はそのままエンターキーを押しても良いです．） -3. これで開いたウィンドウで ``Open documentation of current project`` をクリックします． +3. これで開いたウィンドウで ``Mathematics in Lean`` をクリックします． TEXT. -/ /- OMIT: diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean index 91c8a6f1..c15c6151 100644 --- a/MIL/C01_Introduction/S02_Overview.lean +++ b/MIL/C01_Introduction/S02_Overview.lean @@ -202,7 +202,7 @@ That said, in this book, our emphasis will be on the use of tactics. OMIT. -/ /- TEXT: -証明を組み立てるうえで，細かいステップごとに段階的にフィードバックを受けられることは，非常に役に立ちます．このため，タクティクを使うと証明項を書き下すよりも早く，簡単に証明を書くことができます．とはいえタクティクスタイルと項スタイルの間に明確な線引きは存在しません:上記の例の ``by rw [hk, mul_left_comm]`` のように，項スタイルの証明の途中にタクティクスタイルの証明を入れることが可能です．そして反対に，この後見ていくようにタクティクスタイルの証明中で短い項による証明を用いるのが便利なこともよくあります．とはいえ，本書ではタクティクの使用に重点を置くこととしています． +証明を組み立てるうえで，細かいステップごとに段階的にフィードバックを受けられることは，非常に役に立ちます．このため，タクティクを使うと証明項を書き下すよりも早く，簡単に証明を書くことができます．とはいえタクティクスタイルと項スタイルの間に明確な線引きは存在しません:上記の例の ``by rw [hk, mul_add]`` のように，項スタイルの証明の途中にタクティクスタイルの証明を入れることが可能です．そして反対に，この後見ていくようにタクティクスタイルの証明中で短い項による証明を用いるのが便利なこともよくあります．とはいえ，本書ではタクティクの使用に重点を置くこととしています． TEXT. -/ /- OMIT: diff --git a/MIL/C02_Basics/S01_Calculating.lean b/MIL/C02_Basics/S01_Calculating.lean index 77282154..c15b560a 100644 --- a/MIL/C02_Basics/S01_Calculating.lean +++ b/MIL/C02_Basics/S01_Calculating.lean @@ -145,7 +145,7 @@ OMIT. -/ .. index:: proof state, local context, goal -カーソルがタクティクスタイルの証明の途中にあるとき，Lean は現在の証明の状態を **Lean infoview** ウィンドウに表示します．カーソルを動かすと，状態が変化するのがわかります．Leanの典型的な証明の状態は以下のようになります： +カーソルがタクティクスタイルの証明の途中にあるとき，Lean は現在の証明の状態を **Lean Infoview** ウィンドウに表示します．カーソルを動かすと，状態が変化するのがわかります．Leanの典型的な証明の状態は以下のようになります： .. code-block:: @@ -570,7 +570,7 @@ occurrence of ``a + b`` with ``c``. OMIT. -/ /- TEXT: -``ring`` タクティクは ``Mathlib.Data.Real.Basic`` をインポートしたときに間接的にインポートされています．しかし，次章では実数以外の構造体の計算にも ``ring`` タクティクが使用できることを解説していきます． ``ring`` は ``import Mathlib.Tactic`` コマンドを使用して明示的にインポートすることができます．他の代数的対象にも同様のタクティクがあることを今後見ていきます． ``nth_rewrite`` と呼ばれる ``rw`` の亜種が存在し，それを使用するとゴール(証明したい命題)の中にある表現のうち特定のものだけを置換することができます．ありうる置換対象は1から順番に列挙されます．次の例では ``nth_rewrite 2 h`` は2番目に出現する ``a + b`` を ``c`` に置換しています． +``ring`` タクティクは ``Mathlib.Data.Real.Basic`` をインポートしたときに間接的にインポートされています．しかし，次章では実数以外の構造体の計算にも ``ring`` タクティクが使用できることを解説していきます． ``ring`` は ``import Mathlib.Tactic`` コマンドを使用して明示的にインポートすることができます．他の代数的対象にも同様のタクティクがあることを今後見ていきます． ``nth_rw`` と呼ばれる ``rw`` の亜種が存在し，それを使用するとゴール(証明したい命題)の中にある表現のうち特定のものだけを置換することができます．ありうる置換対象は1から順番に列挙されます．次の例では ``nth_rw 2 h`` は2番目に出現する ``a + b`` を ``c`` に置換しています． EXAMPLES: -/ -- QUOTE: diff --git a/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean b/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean index b4e9387b..2f2377d3 100644 --- a/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean +++ b/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean @@ -249,7 +249,7 @@ but for now we will stick to examples that don't require the case split. OMIT. -/ /- TEXT: -乗法が加法に対して分配法則を満たすように ``min`` 関数が ``max`` に対して分配法則を満たし，その逆も成り立つというのは興味深い事実です．言い換えれば，実数上において ``min a (max b c) ≤ max (min a b) (min a c)`` が成り立ち，この式の ``max`` と ``min`` を入れ替えた同様の式も成り立つということです．しかし次の節では， ``≤`` の推移性と反射性，そして上記で示した ``min`` と ``max`` を特徴付ける性質からこれが **成り立たない** ことを見ていきます．この性質を示すには実数上の関係 ``≤`` が **全順序** （total order）であること，つまり ``∀ x y, x ≤ y ∨ y ≤ x`` という性質が成り立つという事実を利用する必要があります．ここで記号 ``∨`` は選言記号で「または」を表します．最初のケースでは ``min x y = x`` となり，2番めのケースでは ``min x y = y`` となります．場合分けを使って証明する方法は :numref:`disjunction` で学びますが，現時点では場合分けをする必要のない例で説明します． +乗法が加法に対して分配法則を満たすように ``min`` 関数が ``max`` に対して分配法則を満たし，その逆も成り立つというのは興味深い事実です．言い換えれば，実数上において ``min a (max b c) = max (min a b) (min a c)`` が成り立ち，この式の ``max`` と ``min`` を入れ替えた同様の式も成り立つということです．しかし次の節では， ``≤`` の推移性と反射性，そして上記で示した ``min`` と ``max`` を特徴付ける性質からこれが **成り立たない** ことを見ていきます．この性質を示すには実数上の関係 ``≤`` が **全順序** （total order）であること，つまり ``∀ x y, x ≤ y ∨ y ≤ x`` という性質が成り立つという事実を利用する必要があります．ここで記号 ``∨`` は選言記号で「または」を表します．最初のケースでは ``min x y = x`` となり，2番めのケースでは ``min x y = y`` となります．場合分けを使って証明する方法は :numref:`disjunction` で学びますが，現時点では場合分けをする必要のない例で説明します． TEXT. -/ /- OMIT: @@ -394,7 +394,7 @@ See if you can guess the names of the theorems you need to prove the following: OMIT. -/ /- TEXT: -最後の例では，指数が自然数であり ``dvd_mul_left`` を ``apply`` することでLeanに ``x^2`` の定義を ``x * x^1`` に展開させています．次の例を証明するのに必要な定理名を推測してみましょう: +最後の例では，指数が自然数であり ``dvd_mul_left`` を ``apply`` することでLeanに ``x^2`` の定義を ``x^1 * x`` に展開させています．次の例を証明するのに必要な定理名を推測してみましょう: TEXT. -/ -- QUOTE: -- BOTH: diff --git a/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean b/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean index 85261fc2..b59c0923 100644 --- a/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean +++ b/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean @@ -29,7 +29,7 @@ like ``≤`` on the real numbers. Lean knows about partial orders: OMIT. -/ /- TEXT: -:numref:`proving_identities_in_algebraic_structures` では，実数上で成り立つ多くの一般的な恒等式が，可換環のようなより一般的な代数的構造のクラスでも成り立つことを確認しました．等式だけでなく，代数的構造を記述するために必要な公理はなんでも表現することができます．例えば **半順序** （partial order）は実数上の ``≤`` のような，集合上の反射的で推移的な二項関係のことです．Leanはこの半順序を表現できます: +:numref:`proving_identities_in_algebraic_structures` では，実数上で成り立つ多くの一般的な恒等式が，可換環のようなより一般的な代数的構造のクラスでも成り立つことを確認しました．等式だけでなく，代数的構造を記述するために必要な公理はなんでも表現することができます．例えば **半順序** （partial order）は実数上の ``≤`` のような，集合上の反射的で推移的かつ反対称的な二項関係のことです．Leanはこの半順序を表現できます: TEXT. -/ section -- QUOTE: diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean index 39529147..ea5023dc 100644 --- a/MIL/C04_Sets_and_Functions/S01_Sets.lean +++ b/MIL/C04_Sets_and_Functions/S01_Sets.lean @@ -439,7 +439,7 @@ and confirm that the proof still works. OMIT. -/ /- TEXT: -この証明を順を追って見て，何が起こっているのか理解してください．そして ``rw [evens, odds]`` の行を削除しても証明がまだ機能することを確認してください． +この証明を順を追って見て，何が起こっているのか理解してください．ここでゴールにある ``¬ Even n`` を保持するために，単純化器に ``Nat.not_even_iff`` を **使わない** よう指示していることに注意してください．そして ``rw [evens, odds]`` の行を削除しても証明がまだ機能することを確認してください． TEXT. -/ /- OMIT: diff --git a/MIL/C04_Sets_and_Functions/S02_Functions.lean b/MIL/C04_Sets_and_Functions/S02_Functions.lean index 47ec59b4..ce84fe38 100644 --- a/MIL/C04_Sets_and_Functions/S02_Functions.lean +++ b/MIL/C04_Sets_and_Functions/S02_Functions.lean @@ -660,7 +660,7 @@ meets the first part of this specification. OMIT. -/ /- TEXT: -``noncomputable section`` と ``open Classical`` の行は古典論理を本質的な意味で使っているため必要です．入力 ``y`` に対して，関数 ``inverse f`` は ``f x = y`` を満たす ``x`` の値があればそれを返し，なければ ``α`` のデフォルトの要素を返します．これは **依存的なif** （dependent if）による構成の例になっています．というのも条件が真の場合，返される値 ``Classical.choose h`` は仮定 ``h`` に依存するからです．条件式 ``if h : e then a else b`` は，等式 ``dif_pos h`` によって ``h : e`` が与えられると ``a`` に書き換えられ，同様に ``dif_neg h`` によって ``h : ¬ e`` が与えられると ``b`` に書き換えられます．定理 ``inverse_spec`` は ``inverse f`` が if 式の条件を満たすことを述べています． +``noncomputable section`` と ``open Classical`` の行は古典論理を本質的な意味で使っているため必要です．入力 ``y`` に対して，関数 ``inverse f`` は ``f x = y`` を満たす ``x`` の値があればそれを返し，なければ ``α`` のデフォルトの要素を返します．これは **依存的なif** （dependent if）による構成の例になっています．というのも条件が真の場合，返される値 ``Classical.choose h`` は仮定 ``h`` に依存するからです．条件式 ``if h : e then a else b`` は，等式 ``dif_pos h`` によって ``h : e`` が与えられると ``a`` に書き換えられ，同様に ``dif_neg h`` によって ``h : ¬ e`` が与えられると ``b`` に書き換えられます．また似たものとして ``if_pos`` と ``if_neg`` というものもあり，これは非依存なifの構成で機能し，これは次節で用いられます．定理 ``inverse_spec`` は ``inverse f`` が if 式の条件を満たすことを述べています． TEXT. -/ /- OMIT: diff --git a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean index 516a2a58..64d89e7d 100644 --- a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean +++ b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean @@ -268,7 +268,7 @@ Notice that rewriting with ``sbAux`` here replaces ``sbAux f g 0`` with the right-hand side of the corresponding defining equation. OMIT. -/ /- TEXT: -以下の証明を見て，大筋をつかめたら残りの部分を埋めてみてください．最後に ``inv_fun_eq`` を使う必要があります．ここで ``sb_aux`` を使って書き直すと ``sb_aux f g 0`` が対応する定義している等式の右辺に置き換わることに注意しましょう． +以下の証明を見て，大筋をつかめたら残りの部分を埋めてみてください．最後に ``invFun_eq`` を使う必要があります．ここで ``sbAux`` を使って書き直すと ``sbAux f g 0`` が対応する定義している等式の右辺に置き換わることに注意しましょう． BOTH: -/ -- QUOTE: theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by @@ -390,7 +390,7 @@ and more readable, but they sometimes require us to do more work. OMIT. -/ /- TEXT: -この証明ではいくつか新しいタクティクを導入しています．まず ``set`` タクティクに注目します．これは ``sb_set f g`` と ``sb_fun f g`` に対してそれぞれ ``A`` と ``h`` という略語を導入するものです．またこの対応を定義する等式に ``A_def`` と ``h_def`` と名付けています．この省略は定義的なものであり，Leanは必要に応じて自動的に省略形を展開することがあります．しかし常に行われるわけではありません．例えば， ``rw`` を使用する場合，一般的には ``A_def`` と ``h_def`` を明示的に使用する必要があります．つまり，定義はトレードオフの関係にあるのです．式をより短く読みやすくすることができますが，時にはより多くの作業が必要に成ります． +この証明ではいくつか新しいタクティクを導入しています．まず ``set`` タクティクに注目します．これは ``sbSet f g`` と ``sb_fun f g`` に対してそれぞれ ``A`` と ``h`` という略語を導入するものです．またこの対応を定義する等式に ``A_def`` と ``h_def`` と名付けています．この省略は定義的なものであり，Leanは必要に応じて自動的に省略形を展開することがあります．しかし常に行われるわけではありません．例えば， ``rw`` を使用する場合，一般的には ``A_def`` と ``h_def`` を明示的に使用する必要があります．つまり，定義はトレードオフの関係にあるのです．式をより短く読みやすくすることができますが，時にはより多くの作業が必要に成ります． TEXT. -/ /- OMIT: diff --git a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean index fe1484ac..f4f0e815 100644 --- a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean +++ b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean @@ -51,7 +51,7 @@ the identifier ``Nat.Coprime``. The ``norm_num`` tactic is smart enough to compute concrete values. OMIT. -/ /- TEXT: -:math:`a / b` が既約分数であるということは， :math:`a` と :math:`b` は共通の因数がない，つまり **互いに素** （coprime）であることを意味します．Mathlibは述語 ``Nat.coprime m n`` を ``Nat.gcd m n = 1`` と定義しています．Leanの無名の射影による記法を使うと， ``s`` と ``t`` が ``Nat`` 型の式であれば， ``Nat.coprime s t`` の代わりに ``s.coprime t`` と書くことができます．これは ``Nat.gcd`` についても同様です．いつものように，Leanはしばしば ``Nat.coptime`` の定義を必要に応じて自動的に展開しますが， ``Nat.coprime`` 識別子を用いて手動で書き換えや単純化することもできます． ``norm_num`` タクティクは具体的な値を計算するにあたって十分な賢さを備えています． +:math:`a / b` が既約分数であるということは， :math:`a` と :math:`b` は共通の因数がない，つまり **互いに素** （coprime）であることを意味します．Mathlibは述語 ``Nat.Coprime m n`` を ``Nat.gcd m n = 1`` と定義しています．Leanの無名の射影による記法を使うと， ``s`` と ``t`` が ``Nat`` 型の式であれば， ``Nat.Coprime s t`` の代わりに ``s.coprime t`` と書くことができます．これは ``Nat.gcd`` についても同様です．いつものように，Leanはしばしば ``Nat.Coprime`` の定義を必要に応じて自動的に展開しますが， ``Nat.Coprime`` 識別子を用いて手動で書き換えや単純化することもできます． ``norm_num`` タクティクは具体的な値を計算するにあたって十分な賢さを備えています． EXAMPLES: -/ -- QUOTE: #print Nat.Coprime @@ -84,7 +84,7 @@ to the natural numbers. OMIT: -/ /- TEXT: -関数 ``gcd`` についてはすでに :numref:`more_on_order_and_divisibility` で説明しました． ``gcd`` には整数用のバージョンも存在します．このような異なる数体系間の関係については後述します．また ``gcd`` 関数や ``Prime`` ， ``coprime`` にはさらに一般的な概念も存在し，一般的な代数構造で意味を持ちます．Leanがこの一般性をどのように管理しているかについては次の章で説明します．それまでにこの節では自然数に限定して説明しましょう． +関数 ``gcd`` についてはすでに :numref:`more_on_order_and_divisibility` で説明しました． ``gcd`` には整数用のバージョンも存在します．このような異なる数体系間の関係については後述します．また ``gcd`` 関数や ``Prime`` ， ``Coprime`` にはさらに一般的な概念も存在し，一般的な代数構造で意味を持ちます．Leanがこの一般性をどのように管理しているかについては次の章で説明します．それまでにこの節では自然数に限定して説明しましょう． TEXT. -/ /- OMIT: @@ -141,7 +141,7 @@ but for reasons that will become clear below, we will simply use ``2 ∣ m`` to express that ``m`` is even. OMIT. -/ /- TEXT: -この事実は上記で行った議論の重要な性質を確立することができます．すなわちある数の2乗が偶数であれば，その数も偶数であるということです．Mathlibは ``Data.Nat.Parity`` にて述語 ``Even`` を定義していますが，後ほど説明する理由から，ここでは ``m`` が偶数であることを表現するために ``2 ∣ m`` を使用します． +この事実は上記で行った議論の重要な性質を確立することができます．すなわちある数の2乗が偶数であれば，その数も偶数であるということです．Mathlibは ``Algebra.Group.Even`` にて述語 ``Even`` を定義していますが，後ほど説明する理由から，ここでは ``m`` が偶数であることを表現するために ``2 ∣ m`` を使用します． EXAMPLES: -/ -- QUOTE: #check Nat.Prime.dvd_mul @@ -313,7 +313,7 @@ and that if ``n`` is equal to the product of another list of prime numbers, then that list is a permutation of ``Nat.primeFactorsList n``. OMIT. -/ /- TEXT: -素因数分解の一意性とは，0以外の自然数は素数の積として一意に書けるというものです．Mathlibにはこの定理が正式に含まれており， ``Nat.factors`` という関数で表現され，与えられた数の素因数を小さい順に並べたリストを返します．Mathlibは ``Nat.primeFactorsList n`` のすべての要素が素数であること，0より大きい ``n`` はその因数の積に等しいこと，そして ``n`` が他の素数のリストの積に等しい場合，そのリストは ``Nat.primeFactorsList n`` の結果を順列に並べ替えたものであることを証明します． +素因数分解の一意性とは，0以外の自然数は素数の積として一意に書けるというものです．Mathlibにはこの定理が正式に含まれており， ``Nat.primeFactorsList`` という関数で表現され，与えられた数の素因数を小さい順に並べたリストを返します．Mathlibは ``Nat.primeFactorsList n`` のすべての要素が素数であること，0より大きい ``n`` はその因数の積に等しいこと，そして ``n`` が他の素数のリストの積に等しい場合，そのリストは ``Nat.primeFactorsList n`` の結果を順列に並べ替えたものであることを証明します． EXAMPLES: -/ -- QUOTE: #check Nat.primeFactorsList @@ -428,7 +428,7 @@ establishes ``r + 1 ≠ 0`` (``succ`` stands for successor). OMIT: -/ /- TEXT: -``Nat.count_factors_mul_of_pos`` を ``r * n^k`` と一緒に使うには， ``r`` が正であることを知っている必要があります．しかし ``r`` が0の場合，以下の定理は自明であり， ``simp`` で簡単に証明できます．そこで証明は場合分けして行うことにします．一つは ``r`` を ``0`` に置き換えるもので，もう一つは ``r`` を ``r.succ`` に置き換えるものです．後者の場合，定理 ``r.succ_ne_zero`` を使うことができ， ``r.succ ≠ 0`` が成立します． +``Nat.count_factors_mul_of_pos`` を ``r * n^k`` と一緒に使うには， ``r`` が正であることを知っている必要があります．しかし ``r`` が0の場合，以下の定理は自明であり， ``simp`` で簡単に証明できます．そこで証明は場合分けして行うことにします． ``rcases r with _ | r`` の行ではゴールを2つのバージョンへと置き換えています；一つは ``r`` を ``0`` に置き換えるもので，もう一つは ``r`` を ``r + 1`` に置き換えるものです．後者の場合，定理 ``r.succ_ne_zero`` を使うことができ， ``r + 1 ≠ 0`` が成立します（ ``succ`` は後続を意味します）． TEXT. -/ /- OMIT: diff --git a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean index 1b74e368..d4ea9167 100644 --- a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean +++ b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean @@ -31,7 +31,7 @@ Hence :math:`p` is greater than :math:`n`. OMIT. -/ /- TEXT: -帰納と再帰の探求を続けるにあたってもう一つの数学的な基本法則，すなわち素数が無限に存在することの証明を行いましょう．これの形式化された形として，すべての自然数 :math:`n` に対して :math:`n` より大きい素数が存在すると言うことができます．これを証明するために， :math:`p` を :math:`n! + 1` の任意の素因数とします．もし， :math:`p` が :math:`n` より小さければ， :math:`n!` も割ることができます．一方で :math:`n! + 1` も割るため， :math:`p` は1も割ることとなり，矛盾します．したがって :math:`p` は :math:`n` より大きいことになります． +帰納と再帰の探求を続けるにあたってもう一つの数学的な基本法則，すなわち素数が無限に存在することの証明を行いましょう．これの形式化された形として，すべての自然数 :math:`n` に対して :math:`n` より大きい素数が存在すると言うことができます．これを証明するために， :math:`p` を :math:`n! + 1` の任意の素因数とします．もし， :math:`p` が :math:`n` 以下ならば， :math:`n!` も割ることができます．一方で :math:`n! + 1` も割るため， :math:`p` は1も割ることとなり，矛盾します．したがって :math:`p` は :math:`n` より大きいことになります． TEXT. -/ /- OMIT: @@ -388,7 +388,7 @@ Step through the beginning of the proof to see the induction unfold, and then finish it off. OMIT. -/ /- TEXT: -この補題を使って素数 ``p`` が素数の有限集合の積を割り切る場合，そのうちの1つを割ることを示すことができます．Mathlibは有限集合の帰納法について便利な原理を提供しています．任意の有限集合 ``s`` の性質が成り立つことを示すには，空集合でその性質が成り立ち，新しい元 ``a ∉ s`` を1つ追加してもその性質が保たれることを示すことで出来るというものです．この原理は ``Finset.induction_on`` として知られています．これを使うように帰納法のタクティクに指示する際には， ``a`` と ``s`` の名前と帰納法のステップの仮定 ``a ∉ s`` の名前，帰納的仮説の名前を指定することもできます．式 ``Finset.insert a s`` は ``s`` と ``a`` の単集合の和を表します．恒等式 ``Finset.prod_empty`` と ``Finset.prod_insert`` は積に関連する書き換えルールです．以下の証明では最初の ``simp`` が ``Finset.prod_empty`` を適用しています．帰納法がどのように展開され，そして完成されるかを見るために証明の冒頭から順を追って確認してください． +この補題を使って素数 ``p`` が素数の有限集合の積を割り切る場合，そのうちの1つと等しいことを示すことができます．Mathlibは有限集合の帰納法について便利な原理を提供しています．任意の有限集合 ``s`` の性質が成り立つことを示すには，空集合でその性質が成り立ち，新しい元 ``a ∉ s`` を1つ追加してもその性質が保たれることを示すことで出来るというものです．この原理は ``Finset.induction_on`` として知られています．これを使うように帰納法のタクティクに指示する際には， ``a`` と ``s`` の名前と帰納法のステップの仮定 ``a ∉ s`` の名前，帰納的仮説の名前を指定することもできます．式 ``Finset.insert a s`` は ``s`` と ``a`` の単集合の和を表します．恒等式 ``Finset.prod_empty`` と ``Finset.prod_insert`` は積に関連する書き換えルールです．以下の証明では最初の ``simp`` が ``Finset.prod_empty`` を適用しています．帰納法がどのように展開され，そして完成されるかを見るために証明の冒頭から順を追って確認してください． BOTH: -/ -- QUOTE: theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) : diff --git a/MIL/C06_Structures/S02_Algebraic_Structures.lean b/MIL/C06_Structures/S02_Algebraic_Structures.lean index 017bbfa5..5f682662 100644 --- a/MIL/C06_Structures/S02_Algebraic_Structures.lean +++ b/MIL/C06_Structures/S02_Algebraic_Structures.lean @@ -31,7 +31,7 @@ TEXT. -/ OMIT. -/ /- TEXT: -#. **半順序集合** （partially ordered set）は集合 :math:`P` と推移律と反対称律を持った :math:`P` 上の二項演算子 :math:`\le` からなります． +#. **半順序集合** （partially ordered set）は集合 :math:`P` と推移律と反射律を持った :math:`P` 上の二項演算子 :math:`\le` からなります． TEXT. -/ /- OMIT: @@ -268,7 +268,7 @@ to add it to the definition. OMIT. -/ /- TEXT: -ここで型 ``α`` は ``group₁`` の定義における **パラメータ** （parameter）であることに注意してください．したがってオブジェクト ``struc : Group₁ α`` は ``α`` 上の群構造であると考えると良いでしょう．他の群の公理から ``mul_left_inv`` と対になる ``mul_right_inv`` が成り立つことは :numref:`proving_identities_in_algebraic_structures` で見たため，定義に追加する必要はありません． +ここで型 ``α`` は ``group₁`` の定義における **パラメータ** （parameter）であることに注意してください．したがってオブジェクト ``struc : Group₁ α`` は ``α`` 上の群構造であると考えると良いでしょう．他の群の公理から ``inv_mul_cancel`` と対になる ``mul_inv_cancel`` が成り立つことは :numref:`proving_identities_in_algebraic_structures` で見たため，定義に追加する必要はありません． TEXT. -/ /- OMIT: @@ -890,7 +890,7 @@ You can find more information in :numref:`hierarchies` and in a OMIT. -/ /- TEXT: -ここで挙げた例は危険です．なぜなら，Leanのライブラリには ``Group (Equiv.Perm α)`` のインスタンスもあり，乗算は任意の群で定義されているからです．そのため，どちらのインスタンスが見つかるかは曖昧です．実際，Leanは明示的に優先順位を指定しない限り，より新しい宣言を優先します．また，ある構造体が別の構造体のインスタンスであることをLeanに伝えるには， ``extends`` キーワードを使う方法もあります．これは例えばMathlibにおいてすべての可換環が環であることの指定に使われています．より詳しい情報は *Theorem Proving in Lean* のクラス推論に関する節 `section on class inference `_ にあります． [#f21]_ +ここで挙げた例は危険です．なぜなら，Leanのライブラリには ``Group (Equiv.Perm α)`` のインスタンスもあり，乗算は任意の群で定義されているからです．そのため，どちらのインスタンスが見つかるかは曖昧です．実際，Leanは明示的に優先順位を指定しない限り，より新しい宣言を優先します．また，ある構造体が別の構造体のインスタンスであることをLeanに伝えるには， ``extends`` キーワードを使う方法もあります．これは例えばMathlibにおいてすべての可換環が環であることの指定に使われています．より詳しい情報は :numref:`hierarchies` の節および *Theorem Proving in Lean* のクラス推論に関する節 `section on class inference `_ にあります． [#f21]_ TEXT. -/ /- OMIT: diff --git a/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean b/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean index e78c76e3..c53f496e 100644 --- a/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean +++ b/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean @@ -205,7 +205,7 @@ the integers. Note that we could easily avoid repeating all this code, but this is not the topic of the current discussion. OMIT. -/ /- TEXT: -もし ``instance : CommRing GaussInt := _`` と入力してvscodeに表示される電球マークをクリックし，Leanに構造体定義のスケルトンを埋めてもらうと，おびただしい数の項目が表示されます．しかし，構造体の定義に飛ぶと，多くのフィールドにはデフォルトの定義があり，これらはLeanが自動的に埋めてくれます．重要なものは以下の定義にあります．それぞれの場合に置いて，関連する恒等式は定義を展開し， ``ext`` を使って恒等式を実部と虚部に戻し，単純化し，必要であれば整数で関連する環の計算を行うことで証明されます．このコードをすべて繰り返さないようにすることは簡単ですが，これは現在の議論のテーマではないことに注意してください． +もし ``instance : CommRing GaussInt := _`` と入力してvscodeに表示される電球マークをクリックし，Leanに構造体定義のスケルトンを埋めてもらうと，おびただしい数の項目が表示されます．しかし，構造体の定義に飛ぶと，多くのフィールドにはデフォルトの定義があり，これらはLeanが自動的に埋めてくれます．重要なものは以下の定義にあります． ``nsmul`` と ``zsmul`` は特殊なものですが，これは次章で説明するため現時点では無視してください．それぞれの場合に置いて，関連する恒等式は定義を展開し， ``ext`` を使って恒等式を実部と虚部に戻し，単純化し，必要であれば整数で関連する環の計算を行うことで証明されます．このコードをすべて繰り返さないようにすることは簡単ですが，これは現在の議論のテーマではないことに注意してください． BOTH: -/ -- QUOTE: instance instCommRing : CommRing GaussInt where @@ -417,7 +417,7 @@ right-hand side as :math:`(u + vi) + (u' + v'i)`, where OMIT. -/ /- TEXT: -実部と虚部は整数ではないかもしれませんが，最も近い整数 :math:`u` と :math:`v` に丸めることが出来ます．丸めた際の余った部分を :math:`u'+v'i` として，右辺の大きさを :math:`(u + vi) + (u' + v'i)` と表現できます．ここで :math:`|u'| \le 1/2` と :math:`|v'| \le 1/2` という条件があることに注意すると以下のようになります． +実部と虚部は整数ではないかもしれませんが，最も近い整数 :math:`u` と :math:`v` に丸めることが出来ます．丸めた際の余った部分を :math:`u'+v'i` として，右辺を :math:`(u + vi) + (u' + v'i)` と表現できます．ここで :math:`|u'| \le 1/2` と :math:`|v'| \le 1/2` という条件があることに注意すると以下のようになります． .. math:: @@ -581,7 +581,7 @@ some of its properties. The proofs are all short. OMIT. -/ /- TEXT: -この節の残りの定義と定理はすべて ``gaussInt`` 名前空間に置くことにします．まず， ``norm`` 関数を定義し，その性質をいくつか定義してみましょう．これらの証明はすべて短く済みます． +この節の残りの定義と定理はすべて ``GaussInt`` 名前空間に置くことにします．まず， ``norm`` 関数を定義し，その性質をいくつか定義してみましょう．これらの証明はすべて短く済みます． BOTH: -/ namespace GaussInt diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean index 9688cecc..5de3102a 100644 --- a/MIL/C07_Hierarchies/S01_Basics.lean +++ b/MIL/C07_Hierarchies/S01_Basics.lean @@ -235,7 +235,7 @@ information to succeed. The successful attempts do involve the instances generat ``extends`` syntax. OMIT. -/ /- TEXT: -次の例では， ``α`` が ``DiaOneClass₁`` 構造を持つことをLeanに伝え， `Dia₁` インスタンスと `One₁` インスタンスの両方を使用するプロパティを定めます．Leanがこれらのインスタンスをどのように見つけるかを観察できるように，トレースオプションを設定しています．これで出力されるようになる結果は既定ではかなり簡潔ですが，黒い矢印で終わる行をクリックすることで詳細が表示されます．この中にはLeanがインスタンスの検索を成功するために十分な型情報を得る前に検索を行って失敗した結果もふくまれます． +次の例では， ``α`` が ``DiaOneClass₁`` 構造を持つことをLeanに伝え， `Dia₁` インスタンスと `One₁` インスタンスの両方を使用するプロパティを定めます．Leanがこれらのインスタンスをどのように見つけるかを観察できるように，トレースオプションを設定しています．これで出力されるようになる結果は既定ではかなり簡潔ですが，黒い矢印で終わる行をクリックすることで詳細が展開されます．この中にはLeanがインスタンスの検索を成功するために十分な型情報を得る前に検索を行って失敗した結果もふくまれます． BOTH: -/ -- QUOTE: diff --git a/MIL/C07_Hierarchies/S02_Morphisms.lean b/MIL/C07_Hierarchies/S02_Morphisms.lean index b6da4c68..949fe457 100644 --- a/MIL/C07_Hierarchies/S02_Morphisms.lean +++ b/MIL/C07_Hierarchies/S02_Morphisms.lean @@ -293,7 +293,7 @@ Let us redefine our ``MonoidHomClass`` on top of this base layer. OMIT. -/ /- TEXT: -本書でのアプローチで残っている問題は， ``toFun`` フィールドとそれに対応する ``CoeFun`` インスタンスと ``coe`` 属性の周りに繰り返しコードが存在することです．また，このパターンは余分なプロパティを持つ関数にのみ使用され，関数への型強制は単射的であるべきだということを記録しておいたほうが良いでしょう．このために，Mathlibは基底クラス ``FunLike`` で抽象化のレイヤーを1つ増やしています．この基底クラスの上に ``MonoidHomClass`` を再定義してみましょう． +本書でのアプローチで残っている問題は， ``toFun`` フィールドとそれに対応する ``CoeFun`` インスタンスと ``coe`` 属性の周りに繰り返しコードが存在することです．また，このパターンは余分なプロパティを持つ関数にのみ使用され，関数への型強制は単射的であるべきだということを記録しておいたほうが良いでしょう．このために，Mathlibは基底クラス `` DFunLike`` （ ``DFun`` は依存関数を意味します）で抽象化のレイヤーを1つ増やしています．この基底クラスの上に ``MonoidHomClass`` を再定義してみましょう． BOTH: -/ -- QUOTE: diff --git a/MIL/C07_Hierarchies/S03_Subobjects.lean b/MIL/C07_Hierarchies/S03_Subobjects.lean index 805a31d7..8be41cde 100644 --- a/MIL/C07_Hierarchies/S03_Subobjects.lean +++ b/MIL/C07_Hierarchies/S03_Subobjects.lean @@ -28,7 +28,7 @@ coercion and ``Membership`` instance. OMIT. -/ /- TEXT: -ある代数構造とその射を定義した後の次なるステップとして，この代数構造を継承する集合，例えば部分群や部分環を考えましょう．これは前回の話題とほぼ重複します．実際， ``X`` の集合は ``X`` から ``Prop`` への関数として実装されるので，部分対象はある述語を満たす関数です．したがって， ``FunLike`` クラスとその子孫のクラスを生み出した多くのアイデアを再利用できます． ``FunLike`` 自体は再利用しません．これをしてしまうと集合 ``X`` から ``X → Prop`` への抽象化の壁を壊してしまうためです．その代わりに ``SetLike`` クラスが存在します．関数型への埋め込みをラップする代わりに，このクラスは ``Set`` 型への埋め込みをラップし，対応する型強制と ``Membership`` インスタンスを定義します． +ある代数構造とその射を定義した後の次なるステップとして，この代数構造を継承する集合，例えば部分群や部分環を考えましょう．これは前回の話題とほぼ重複します．実際， ``X`` の集合は ``X`` から ``Prop`` への関数として実装されるので，部分対象はある述語を満たす関数です．したがって， ``DFunLike`` クラスとその子孫のクラスを生み出した多くのアイデアを再利用できます． ``DFunLike`` 自体は再利用しません．これをしてしまうと集合 ``X`` から ``X → Prop`` への抽象化の壁を壊してしまうためです．その代わりに ``SetLike`` クラスが存在します．関数型への埋め込みをラップする代わりに，このクラスは ``Set`` 型への埋め込みをラップし，対応する型強制と ``Membership`` インスタンスを定義します． BOTH: -/ -- QUOTE: diff --git a/MIL/C09_Topology/S01_Filters.lean b/MIL/C09_Topology/S01_Filters.lean index ead76106..d7e6ff50 100644 --- a/MIL/C09_Topology/S01_Filters.lean +++ b/MIL/C09_Topology/S01_Filters.lean @@ -536,7 +536,7 @@ Putting these pieces together gives us essentially the notion of convergence that we used in :numref:`sequences_and_convergence`. OMIT. -/ /- TEXT: -またフィルタ ``atTop`` に対する良い基底もあります．補題 ``Filter.has_basis.tendsto_iff`` を使えば， ``F`` と ``G`` の基底が与えられたときに， ``Tendsto f F G`` という形の文を再形式化することができます．これらをまとめると， :numref:`sequences_and_convergence` で取り扱った収束の本質的な概念が得られます． +またフィルタ ``atTop`` に対する良い基底もあります．補題 ``Filter.HasBasis.tendsto_iff`` を使えば， ``F`` と ``G`` の基底が与えられたときに， ``Tendsto f F G`` という形の文を再形式化することができます．これらをまとめると， :numref:`sequences_and_convergence` で取り扱った収束の本質的な概念が得られます． EXAMPLES: -/ -- QUOTE: example (u : ℕ → ℝ) (x₀ : ℝ) : diff --git a/MIL/C09_Topology/S03_Topological_Spaces.lean b/MIL/C09_Topology/S03_Topological_Spaces.lean index 43b6addd..ccc81f8d 100644 --- a/MIL/C09_Topology/S03_Topological_Spaces.lean +++ b/MIL/C09_Topology/S03_Topological_Spaces.lean @@ -259,7 +259,7 @@ a map ``f : X → (ℝ → ℝ)`` is continuous if and only if ``fun x ↦ f x t OMIT. -/ /- TEXT: -特に，距離空間の商や，距離空間の不可算積上の実用的な距離は存在しません．例えば ``ℝ → ℝ`` という型を考えてみましょう．これは ``ℝ`` をインデックスとする ``ℝ`` のコピーの積として見ることができます．関数列の点ごとの収束は，立派に収束の概念であると言いたいところです．しかし， ``ℝ → ℝ`` 上にはこの収束の概念を与える距離は存在しません．これに関連して，写像 ``f : X → (ℝ → ℝ)`` がすべての ``t : ℝ`` に対して ``fun x ↦ f x t`` が連続である場合だけ連続であることを保証する距離は存在しません． +特に，距離空間の商や，距離空間の不可算積上の実用的な距離は存在しません．例えば ``ℝ → ℝ`` という型を考えてみましょう．これは ``ℝ`` をインデックスとする ``ℝ`` のコピーの積として見ることができます．関数列の点ごとの収束は，立派に収束の概念であると言いたいところです．しかし， ``ℝ → ℝ`` 上にはこの収束の概念を与える距離は存在しません．これに関連して，写像 ``f : X → (ℝ → ℝ)`` がすべての ``t : ℝ`` に対して ``fun x ↦ f x t`` が連続である場合に限り連続であることを保証する距離は存在しません． TEXT. -/ /- OMIT: diff --git a/README.md b/README.md index ba458299..2537da99 100644 --- a/README.md +++ b/README.md @@ -97,28 +97,36 @@ | S02_Morphisms.lean | [s-taiga](https://github.com/s-taiga) | | S03_Subobjects.lean | [s-taiga](https://github.com/s-taiga) | -* C08_Topology +* C08_Groups_and_Rings | 章名 | 担当 | | --- | --- | -| C08_Topology.rst | [s-taiga](https://github.com/s-taiga) | +| C08_Groups_and_Rings.rst | [s-taiga](https://github.com/s-taiga) | +| S01_Groups.lean | [s-taiga](https://github.com/s-taiga) | +| S02_Rings.lean | [s-taiga](https://github.com/s-taiga) | + +* C09_Topology + +| 章名 | 担当 | +| --- | --- | +| C09_Topology.rst | [s-taiga](https://github.com/s-taiga) | | S01_Filters.lean | [s-taiga](https://github.com/s-taiga) | | S02_Metric_Spaces.lean | [s-taiga](https://github.com/s-taiga) | | S03_Topological_Spaces.lean | [s-taiga](https://github.com/s-taiga) | -* C09_Differential_Calculus +* C10_Differential_Calculus | 章名 | 担当 | | --- | --- | -| C09_Differential_Calculus.rst | [s-taiga](https://github.com/s-taiga) | +| C10_Differential_Calculus.rst | [s-taiga](https://github.com/s-taiga) | | S01_Elementary_Differential_Calculus.lean | [s-taiga](https://github.com/s-taiga) | | S02_Differential_Calculus_in_Normed_Spaces.lean | [s-taiga](https://github.com/s-taiga) | -* C10_Integration_and_Measure_Theory +* C11_Integration_and_Measure_Theory | 章名 | 担当 | | --- | --- | -| C10_Integration_and_Measure_Theory.rst | [s-taiga](https://github.com/s-taiga) | +| C11_Integration_and_Measure_Theory.rst | [s-taiga](https://github.com/s-taiga) | | S01_Elementary_Integration.lean | [s-taiga](https://github.com/s-taiga) | | S02_Measure_Theory.lean | [s-taiga](https://github.com/s-taiga) | | S03_Integration.lean | [s-taiga](https://github.com/s-taiga) | diff --git a/scripts/mkdoc.py b/scripts/mkdoc.py index 22ee60ea..70ebb278 100755 --- a/scripts/mkdoc.py +++ b/scripts/mkdoc.py @@ -101,7 +101,7 @@ def make_lean_user_main_import_file(): バージョン情報 -------------- -この翻訳は原文のcommit `2bba5592ebfb3075ca1fd4d12843d2bf197bb0d1 `_ に基づいています． +この翻訳は原文のcommit `dd607c678b229e26cd6c8dbe43e56f5455b39210 `_ に基づいています． """