From d62618616693444d1ba3b85cfe835632eb0e8df7 Mon Sep 17 00:00:00 2001 From: aconite-ac Date: Sat, 9 Sep 2023 23:06:09 +0900 Subject: [PATCH] =?UTF-8?q?=E5=8F=A5=E8=AA=AD=E7=82=B9=E3=81=AE=E8=AA=A4?= =?UTF-8?q?=E3=82=8A=E3=82=92=E5=BE=AE=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/c3_universes_types_terms.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/c3_universes_types_terms.md b/src/c3_universes_types_terms.md index cef2041..c89d685 100644 --- a/src/c3_universes_types_terms.md +++ b/src/c3_universes_types_terms.md @@ -15,7 +15,7 @@ いま $\pi$ は項ですが，型ではありません. Lean では `x : π` は意味を持ちません．集合論では， $x\in\pi$ は意味を持ちますが，これは集合論において全てが集合であることに起因する，奇妙な偶然です． さらに，$\pi$ の実際の要素は， -実数がどのように実装されるか（たとえばデデキント切断としてか、コーシー数列としてか） +実数がどのように実装されるか（たとえばデデキント切断としてか，コーシー数列としてか） に依存するため，集合論での $x\in\pi$ は，構文的には意味を持つものの，数学的な意味はありません． たまたま意味をなすだけで，システムの癖に過ぎません．もし「 $x \in \pi$ には意味があるはずだ」 とあなたが断固として言うなら，「あなたは集合論に洗脳されているのだ」と私は言うでしょう．