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