【無限小】柄谷行人を解体する80【偏微分∂】 (965ﾚｽ)

【無限小】柄谷行人を解体する80【偏微分∂】 http://lavender.5ch.net/test/read.cgi/philo/1729771657/

上下前次1-新
通常表示 512ﾊﾞｲﾄ分割 ﾚｽ栞

---

530: 考える名無しさん [age] 2024/11/06(水) 21:04:08.08 ID:0 From mathcomp Require Import all_ssreflect. (* 2要素を持つ順序数型の濃度 *) Lemma bool_cardinal : #|'I_2| = 2. Proof. by rewrite card_ord. Qed. 1 subgoal ______________________________________(1/1) #|'I_2| = 2 私:型'I_2は、自然数nに対応する順序数ord(n)の形式化として、 n : natに対し型'I_nが与えられる。つまり、上記の例は ブール型なので、0<1という順序数となり、濃度は2になる、 という言明ですよね。 AI:はい、その通りです！ 'I_2 は {0,1} という2要素の順序集合を 表しているんですね。では、空集合（濃度0）の例として、'I_0 を 使ってみましょう： http://lavender.5ch.net/test/read.cgi/philo/1729771657/530

---

上下前次1-新書関写板覧索設栞歴

---

あと 435 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ

---

Google検索

Wikipedia

---

ぬこの手 ぬこTOP 0.007s