:
目次
目次
mizarと集合論
師玉康成
目次
TARSKIの公理系
TARSKI.miz
外延性の公理
非順序対の定義
包含関係の定義
集合の合弁の定義
正則性の公理
選出の公理(Fraenkelの公理式)
順序対の定義
集合の等濃度の定義
Tarskiの公理
xbool.0.miz
分出公理
空集合の定義と一意性
集合
の合弁
集合
の共通部分
集合
から
の要素を除いた差集合
空集合
排他論理和
互いに素(交わらない)集合
真部分集合
比較可能な集合
集合の等号 = の再定義
排他和の定理
定理
の宣言
定理
定理
定理
xboole1.miz
BOOLE'1
BOOLE'2
theorem BOOLE'29: :: BOOLE'29:
theorem BOOLE'27: :: BOOLE'27:
theorem BOOLE'30: :: BOOLE'30:
theorem BOOLE'64: :: BOOLE'64:
theorem :: SYSREL'2:
theorem :: SYSREL'3:
theorem BOOLE'31: :: BOOLE'31:
theorem BOOLE'32: :: BOOLE'32:
theorem BOOLE'33: :: BOOLE'33:
theorem :: AMI_5'2 :
theorem :: SETWISEO'7:
theorem BOOLE'35: :: BOOLE'35:
theorem :: BOOLE'34:
theorem :: BOOLE'56:
theorem :: BOOLE'59:
theorem BOOLE'67: :: BOOLE'67:
theorem BOOLE'37: :: BOOLE'37:
theorem :: SYSREL'4:
theorem BOOLE'39: :: BOOLE'39:
theorem :: BOOLE'57:
theorem :: BOOLE'68:
theorem BOOLE'69: :: BOOLE'69:
theorem BOOLE'70: :: BOOLE'70:
theorem BOOLE'71: :: BOOLE'71:
theorem :: BOOLE'72:
theorem BOOLE'40: :: BOOLE'40:
theorem :: BOOLE'41:
theorem BOOLE'42: :: BOOLE'42:
theorem :: BOOLE'38:
theorem :: BOOLE'44:
theorem :: BOOLE'53:
theorem :: BOOLE'45:
theorem :: BOOLE'90:
theorem BOOLE'46: :: BOOLE'46:
theorem BOOLE'47: :: BOOLE'47:
theorem BOOLE'86:
この文書について...
Yasunari SHIDAMA
の合弁 
から
の要素を除いた差集合
の宣言
