【無限小】柄谷行人を解体する80【偏微分∂】 (925ﾚｽ)
上下前次1-新
530: [age] 11/06(水)21:04 ID:0(530/925) 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)の形式化として、
n : natに対し型'I_nが与えられる。つまり、上記の例は
ブール型なので、0<1という順序数となり、濃度は2になる、
という言明ですよね。
AI:はい、その通りです！ 'I_2 は {0,1} という2要素の順序集合を
表しているんですね。では、空集合（濃度0）の例として、'I_0 を
使ってみましょう：
上下前次1-新書関写板覧索設栞歴
あと 395 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.005s