C08/S01翻訳完了

GLOSSARY.md

@@ -21,6 +21,7 @@
 | cauchy sequence | コーシー列 |
 | closed sets | 閉集合 |
 | closure | 閉包 |
+| closure property | 閉性 |
 | change-of-variables | 変数変換 |
 | chapter | 章 |
 | cluster point | 集積点 |
@@ -35,6 +36,7 @@
 | convergence | 収束 |
 | coprime | 互いに素 |
 | curly brackets | 波括弧 |
+| cycle | 巡回置換 |
 | dense | 稠密 |
 | dependent type theory | 依存型理論 |
 | derivative function | 導関数 |
@@ -58,11 +60,15 @@
 | filter | フィルタ |
 | filter basis | フィルタ基底 |
 | first countability | 第一可算 |
+| free group | 自由群 |
 | functoriality | 関手性 |
+| full subgroup | 完全部分群 |
 | Galois connection | ガロア接続 |
 | gaussian integer | ガウス整数 |
 | greatest common divisor | 最大公約数 |
 | greatest lower bound | 最大下界 |
+| group action | 群作用 |
+| group presentation | 群の表示 |
 | higher-order unification | 高階ユニフィケーション |
 | identity | 恒等式, 等式 |
 | if-and-only-if statement | 同値性を主張する文 |
@@ -85,6 +91,7 @@
 | mass | 体積量 |
 | measure theory | 測度論 |
 | meet | 交わり |
+| membership | 帰属 |
 | metric space | 距離空間 |
 | metric space topology | 距離空間位相 |
 | module | 加群 |
@@ -102,10 +109,12 @@
 | open sets | 開集合 |
 | operator | 演算子（中置記法の定義等なにかしら特殊な記法が用意されている場合）、関数（それ以外） |
 | operator norm | 作用素ノルム |
+| orbit | 軌道（群論） |
 | ordered ring | 順序環 |
 | preimage | 逆像 |
 | partial order | 半順序 |
 | partially bundled structure | 部分的に束ねられた構造体 |
+| permutations | 置換 |
 | principal filter | 主フィルタ |
 | proof term | 証明項 |
 | proof by contradiction | 背理法 |
@@ -125,6 +134,7 @@
 | simplify | 単純化 |
 | simplifier | ``simp``  |
 | singleton | 単集合 |
+| stabilizer | 固定部分群（群論） |
 | statement | 命題 |
 | strictly differentiable | 狭義微分可能 |
 | strict partial order | 狭義半順序 |
@@ -134,17 +144,21 @@
 | support | 台 |
 | supremum | 上限 |
 | surjective | 全射 |
+| symmetric group | 対称群 |
 | tend to ~ | ~に収束する |
 | topological group | 位相群 |
 | topological space | 位相空間 |
 | total order | 全順序 |
 | transitivity | 推移性 |
+| translation | 移動作用（群論） |
 | triangle inequality | 三角不等式 |
+| type ascription | 型アスクリプション |
 | uncountable | 不可算 |
 | Uniform Boundedness Principle | 一様有界性原理 |
 | uniformly continuous | 一様連続 |
 | uniform space | 一様空間 |
 | union | 合併, 非交和 |
+| universal property | 普遍性 |
 | universal quantifier | 全称量化子 |
 | well-founded | 整礎関係 |
 | well-formed | 合法 |

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -39,7 +39,7 @@ You can type ``∈`` as ``\in`` or ``\mem`` and ``∉`` as ``\notin``.
 
 OMIT. -/
 /- TEXT:
-``α`` が型であるとき， ``Set α`` 型は ``α`` の要素からなる集合の集まりです．この型は通常の集合論的な操作や関係をサポートしています．例えば ``s ⊆ t`` は ``s`` が ``t`` の部分集合であること， ``s ∩ t`` は ``s`` と ``t`` の共通部分， ``s ∪ t`` は ``s`` と ``t`` の合併を表します．部分集合の関係は ``\ss`` か ``\sub`` で，共通部分は ``\i`` もしくは ``\cap`` ，合併は ``\un`` か ``\cup`` で入力できます．またMathlibは ``univ`` という集合も定義しています．これは ``α`` のすべての要素からなる集合です．そして ``\empty`` で入力される空集合 ``∅`` も定義しています． ``x : α`` と ``s : Set α`` が与えられた時，式 ``x ∈ s`` は ``x`` が ``s`` のメンバーであることを表します．集合の所属関係に言及する定理は，しばしばその名前に ``mem`` を含みます．式 ``x ∉ s`` は ``¬ x ∈ s`` を省略したものです． ``∈`` は ``\in`` か ``\mem`` で， ``∉`` は ``\notin`` で入力できます．
+``α`` が型であるとき， ``Set α`` 型は ``α`` の要素からなる集合の集まりです．この型は通常の集合論的な操作や関係をサポートしています．例えば ``s ⊆ t`` は ``s`` が ``t`` の部分集合であること， ``s ∩ t`` は ``s`` と ``t`` の共通部分， ``s ∪ t`` は ``s`` と ``t`` の合併を表します．部分集合の関係は ``\ss`` か ``\sub`` で，共通部分は ``\i`` もしくは ``\cap`` ，合併は ``\un`` か ``\cup`` で入力できます．またMathlibは ``univ`` という集合も定義しています．これは ``α`` のすべての要素からなる集合です．そして ``\empty`` で入力される空集合 ``∅`` も定義しています． ``x : α`` と ``s : Set α`` が与えられた時，式 ``x ∈ s`` は ``x`` が ``s`` のメンバーであることを表します．集合の帰属関係に言及する定理は，しばしばその名前に ``mem`` を含みます．式 ``x ∉ s`` は ``¬ x ∈ s`` を省略したものです． ``∈`` は ``\in`` か ``\mem`` で， ``∉`` は ``\notin`` で入力できます．
 
 .. index:: simp, tactics ; simp
 

MIL/C07_Hierarchies/S01_Basics.lean

@@ -89,7 +89,7 @@ index that would be useful to distinguish between several unknown things). Anoth
 to avoid this issue would be to use a type annotation, as in:
 OMIT. -/
 /- TEXT:
-もう一つの注意点は，Leanが ``α`` がなんであるかを知っている場合にのみ，この操作は機能するという点です．上の例で全体の型 ``: α`` を省略すると ``typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α)`` というようなエラーメッセージが表示されます．ここで ``?m.263 α`` は「 ``α`` に依存する何らかの型」を意味します．（263は単に自動生成されたインデックスで，未知のものを区別するのに便利です）この問題を避けるもう一つの方法は，次のように型注釈を使うことです:
+もう一つの注意点は，Leanが ``α`` がなんであるかを知っている場合にのみ，この操作は機能するという点です．上の例で型アスクリプション ``: α`` を省略すると ``typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α)`` というようなエラーメッセージが表示されます．ここで ``?m.263 α`` は「 ``α`` に依存する何らかの型」を意味します．（263は単に自動生成されたインデックスで，未知のものを区別するのに便利です）この問題を避けるもう一つの方法は，次のように型注釈を使うことです:
 BOTH: -/
 -- QUOTE:
 example (α : Type) [One₁ α] := (One₁.one : α)