タイポの修正

lean-ja · Aug 25, 2024 · 73bcc97 · 73bcc97
1 parent aa9d8a4
commit 73bcc97
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Examples/Exercise/CantorTheorem.lean b/Examples/Exercise/CantorTheorem.lean
@@ -51,9 +51,9 @@ def Set.union (A B : Set α) : Set α := fun x => x ∈ A ∨ x ∈ B
 
 ### 内包記法の定義
 
-「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{ x : α | p x}` が使用できるようにしましょう。
+「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{x : α | p x}` が使用できるようにしましょう。
 
-Lean のメタプログラミングフレームワークの力を借りれれば、そうしたことも可能です。
+Lean のメタプログラミングフレームワークの力を借りれば、そうしたことも可能です。
 -/
 section --#
 

diff --git a/Examples/Solution/CantorTheorem.lean b/Examples/Solution/CantorTheorem.lean
@@ -51,9 +51,9 @@ def Set.union (A B : Set α) : Set α := fun x => x ∈ A ∨ x ∈ B
 
 ### 内包記法の定義
 
-「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{ x : α | p x}` が使用できるようにしましょう。
+「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{x : α | p x}` が使用できるようにしましょう。
 
-Lean のメタプログラミングフレームワークの力を借りれれば、そうしたことも可能です。
+Lean のメタプログラミングフレームワークの力を借りれば、そうしたことも可能です。
 -/
 section --#