【無限小】柄谷行人を解体する80【偏微分∂】 (925ﾚｽ)
上下前次1-新

---

546: [age] 11/06(水)21:25 ID:0(546/925) AA×


[240|320|480|600|100%|JPG|べ|ﾚｽ栞|ﾚｽ消]
546: [age] 2024/11/06(水) 21:25:45.42 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/546
要素を持つ順序数型の濃度 私型は自然数に対応する順序数の形式化として に対し型が与えられるつまり上記の例は ブール型なのでという順序数となり濃度はになる という言明ですよね はいその通りです！ は という要素の順序集合を 表しているんですねでは空集合濃度の例として を 使ってみましょう

---

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

---

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

---

ぬこの手 ぬこTOP 0.021s