Skip to content

Commit

Permalink
句読点の誤りを微修正
Browse files Browse the repository at this point in the history
  • Loading branch information
aconite-ac committed Sep 9, 2023
1 parent 82c89ff commit d626186
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/c3_universes_types_terms.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
いま $\pi$ は項ですが,型ではありません. Lean では `x : π` は意味を持ちません.集合論では,
$x\in\pi$ は意味を持ちますが,これは集合論において全てが集合であることに起因する,奇妙な偶然です.
さらに,$\pi$ の実際の要素は,
実数がどのように実装されるか(たとえばデデキント切断としてかコーシー数列としてか)
実数がどのように実装されるか(たとえばデデキント切断としてかコーシー数列としてか)
に依存するため,集合論での $x\in\pi$ は,構文的には意味を持つものの,数学的な意味はありません.
たまたま意味をなすだけで,システムの癖に過ぎません.もし「 $x \in \pi$ には意味があるはずだ」
とあなたが断固として言うなら,「あなたは集合論に洗脳されているのだ」と私は言うでしょう.
Expand Down

0 comments on commit d626186

Please sign in to comment.