[過去ﾛｸﾞ] 【無限小】柄谷行人を解体する80【偏微分∂】 (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
547: [age] 11/06(水)21:26 ID:0(547/1000) AAS
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
上下前次1-新書関写板覧索設栞歴
あと 455 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.008s