空集合

• 空集合に関して。
• ファイルは、a3Emp01.v
• いかなる集合も要素に持たない集合が存在することを公理は主張している。

Require Export Intui.
Require Export a1Axset.

(*空集合が存在するとしたら唯一*)
Theorem Empuni : Set_eq -> ExEmp ->
  exists! y:Set, forall x:Set, ~ (x /e y).
Proof.
 intros Hse (y,Hee).
 exists y.
 red.
 split.
 assumption.
 intros z Hez.
 apply Hse.
 split.
 intros x Hy.
 apply False_ind.
 apply (Hee x).
 assumption.
 intros x Hz.
 apply False_ind.
 apply (Hez x).
 assumption.
Qed.

(* 空集合を現す定数を定義できる *)
上記の定理Empuniを根拠にして、空集合を現す関数記号Empを導入できる。それは、 Nota.vでなされている。

(*空集合は全てのクラスの部分クラス*)
Theorem Empcall : PrEmp -> forall (T:Type)(A:T), (Emp /c= A).
Proof.
 intros Hpe T A x He.
 apply False_ind.
 apply (Hpe x).
 assumption.
Qed.

(*空集合に等しくなる条件*)
Theorem Empeq : PrEmp ->
 forall (T:Type)(A:T), (forall x:Set, ~ (x /e A)) -> (A /= Emp).
Proof.
 intros Hpe T A H.
 split.
 intros x HA.
 apply False_ind.
 apply (H x).
 assumption.
 intros x He.
 apply False_ind.
 apply (Hpe x).
 assumption.
Qed.

もどる