[過去ﾛｸﾞ] 【無限小】柄谷行人を解体する80【偏微分∂】 (1002ﾚｽ)

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

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

---

このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ

---

547: 考える名無しさん [age] 2024/11/06(水) 21:26:26.50 ID:0 From mathcomp Require Import all_ssreflect. (* 空集合（0要素の順序数型）の濃度 *) Lemma empty_cardinal : #|'I_0| = 0. Proof. by rewrite card_ord. Qed. このコードでは： 1. 'I_2 は {0,1} という2要素の順序集合 2. 'I_0 は要素を持たない空集合を表現 3. どちらも card_ord という補題で証明できます 'I_nという型は、0以上n未満の自然数を要素として 持つ型なので、n=0の場合は要素が存在せず、空集合となります。 これは直感的にも分かりやすい空集合の例となっていますね！ 1 subgoal ______________________________________(1/1) #|'I_2| = 2 1 subgoal ______________________________________(1/1) #|'I_0| = 0 http://lavender.5ch.net/test/read.cgi/philo/1729771657/547

---

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

---

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

---

Google検索

Wikipedia

---

ぬこの手 ぬこTOP 0.009s