集合の相等

• 集合と集合、あるいはクラスとクラスが等しいということに関する定理の集まりである。
• ファイルは、a0Seteq.v

Require Export Intui.
Require Export Nota.

• 前もって、Intui.v、Nota.vをそれぞれコンパイルしたIntui.vo、Nota.voが同じフォルダにないと、エラーになります。

Theorem Subc_refl : forall (T:Type)(A:T), A /c= A.
Proof.
 intros T A x H.
 assumption.
Qed.

• A⊆Aの証明である。

Theorem Subc_trans : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /c= b) -> (b /c= c) -> (a /c= c).
Proof.
 intros A B C a b c Hab Hbc x Ha.
 apply Hbc.
 apply Hab.
 assumption.
Qed.

Theorem Eqcl_refl : forall (T:Type)(A:T), A /= A.
Proof.
 intros T A.
 split.
 apply Subc_refl.
 apply Subc_refl.
Qed.

• A = Aの意味をもつ別の表現A /= Aを導入してしまっているので、このような定理も証明しないといけない。
• いずれ集合論の公理（Set_eq）によって、A = AとA /= Aは同値となる。
• 「/=」は「集合として等しい」という意味の記号である。斜めの線があるが、「等しくない」と読み間違わないように。

Theorem Eqcl_sym : forall (A B:Type)(a:A)(b:B),
 (a /= b) -> (b /= a).
Proof.
 intros A B a b (Hab,Hba).
 split; assumption.
Qed.

Theorem Eqcl_trans : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /= b) -> (b /= c) -> (a /= c).
Proof.
 intros A B C a b c Hab Hbc.
 elim Hab; intros Hcab Hcba.
 elim Hbc; intros Hcbc Hccb.
 split.
 apply Subc_trans with (b := b).
 assumption.
 assumption.
 apply Subc_trans with (b := b).
 assumption.
 assumption.
Qed.

(*真部分クラス*)
Theorem Cl_psub_not : forall (A B:Type)(a:A)(b:B),
 (a /cc b) -> ((a /c= b) /\ ~ (a /= b)).
Proof.
 intros A B a b Hcc.
 split.
 elim Hcc; intros H1 H2.
 assumption.
 (*unfold Eqcl.*)
 intros (H3,H4).
 elim Hcc; intros H1 H2.
 elim H2.
 assumption.
Qed.

Theorem Cl_not_psub : forall (A B:Type)(a:A)(b:B),
 (a /c= b) -> (~ (a /= b)) -> (a /cc b).
Proof.
 intros A B a b Hce Hne.
 split.
 exact Hce.
 intro Hba.
 elim Hne.
 split; assumption.
Qed.

Theorem Psub_irrefl : forall (T:Type)(A:T), ~ (A /cc A).
Proof.
 intros T A (H1,H2).
 elim H2.
 assumption.
Qed.

Theorem Psub_sub_n : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /cc b) -> (b /c= c) -> ~ (c /c= a).
Proof.
 intros A B C a b c (Hcab,Hcba) Hbc Hca.
 elim Hcba.
 apply Subc_trans with (b := c).
 assumption.
 assumption.
Qed.

Theorem Sub_psub_n : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /c= b) -> (b /cc c) -> ~ (c /c= a).
Proof.
 intros A B C a b c Hab (Hcbc,Hccb) Hca.
 elim Hccb.
 apply Subc_trans with (b := a).
 assumption.
 assumption.
Qed.

Theorem Psub_psub_n : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /cc b) -> (b /cc c) -> ~ (c /c= a).
Proof.
 intros A B C a b c (Hcab,Hcba) (Hcbc,Hccb) Hca.
 elim Hcba.
 apply Subc_trans with (b := c).
 assumption.
 assumption.
Qed.

Theorem Psub_sub_p : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /cc b) -> (b /c= c) -> (a /cc c).
Proof.
 intros A B C a b c (Hcab,Hcba) Hbc.
 split.
 apply Subc_trans with (b := b).
 assumption.
 assumption.
 apply Psub_sub_n with (b := b).
 split.
 assumption.
 assumption.
 assumption.
Qed.

Theorem Sub_psub_p : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /c= b) -> (b /cc c) -> (a /cc c).
Proof.
 intros A B C a b c Hab (Hcbc,Hccb).
 split.
 apply Subc_trans with (b := b).
 assumption.
 assumption.
 apply Sub_psub_n with (b := b).
 assumption.
 split.
 assumption.
 assumption.
Qed.

Theorem Psub_psub_p : forall (A B C:Type)(a:A)(b:B)(c:C),
 (a /cc b) -> (b /cc c) -> (a /cc c).
Proof.
 intros A B C a b c (Hcab,Hcba) (Hcbc,Hccb).
 split.
 apply Subc_trans with (b := b).
 assumption.
 assumption.
 apply Psub_sub_n with (b := b).
 split.
 assumption.
 assumption.
 assumption.
Qed.

もどる