対集合

• 対集合に関して。
• ファイルは、a4Pair01.v
• 2つの集合があるとき、その2つのみを要素とする集合が存在することを公理は主張している。

Require Export a2Seteq2.

(*対集合の唯一性*)
Theorem SPairuni : Set_eq -> SPair ->
 forall a b:Set, exists! y:Set, forall x:Set,
 (x /e y) <-> ((x = a) \/ (x = b)).
Proof.
 intros Hse Hsp a b.
 apply Ex2uni.
 exact Hse.
 apply Hsp.
Qed.

(* 対集合を現す定数を定義できる *)
上記の定理SPairuniを根拠にして、対集合を現す関数記号SetPair(Notationは{ a , b })を導入できる。それは、 Nota.vでなされている。

(*対集合の対称性*)
Theorem SPaircom : Set_eq -> SPairf ->
 forall a b:Set, { a , b } = { b , a }.
Proof.
 intros Hse Hsp a b.
 apply Hse.
 split.
 intros x Hab.
 cut ((x = b) \/ (x = a)).
 cut (x /e {b, a} <-> x = b \/ x = a).
 intros (H1,H2); assumption.
 apply Hsp.
 cut ((x = a) \/ (x = b)).
 apply Orcomr.
 generalize Hab.
 cut (x /e {a, b} <-> x = a \/ x = b).
 intros (H1,H2); assumption.
 apply Hsp.
 intros x Hba.
 cut ((x = a) \/ (x = b)).
 cut (x /e {a, b} <-> x = a \/ x = b).
 intros (H1,H2); assumption.
 apply Hsp.
 cut ((x = b) \/ (x = a)).
 apply Orcomr.
 generalize Hba.
 cut (x /e {b, a} <-> x = b \/ x = a).
 intros (H1,H2); assumption.
 apply Hsp.
Qed.

		SPairf
		x∈{a, b} <-> x = a∨x = b
	[H:x∈{a, b}]	x∈{a, b} -> x = a∨x = b				SPairf
	x = a∨x = b				Orcomr	x∈{b, a} <-> x = b∨x = a
				x = b∨x = a		x = b∨x = a -> x∈{b, a}
		右と同様		x∈{b, a}			H
		{b, a}⊆{a, b}		{a, b}⊆{b, a}
	Set_eq	{a, b} /= {b, a}
	{a, b} = {b, a}

(*対集合の基本1*)
Theorem SPairPrl : SPairf ->
 forall a b:Set, a /e { a , b }.
Proof.
 intros Hsp a b.
 cut ((a = a) \/ (a = b)).
 cut (a /e { a , b } <-> (a = a) \/ (a = b)).
 intros (H1,H2); assumption.
 apply Hsp.
 left.
 reflexivity.
Qed.

(*対集合の基本2*)
Theorem SPairPrr : SPairf ->
 forall a b:Set, b /e { a , b }.
Proof.
 intros Hsp a b.
 cut ((b = a) \/ (b = b)).
 cut (b /e { a , b } <-> (b = a) \/ (b = b)).
 intros (H1,H2); assumption.
 apply Hsp.
 right.
 reflexivity.
Qed.

(*-------------------------------------------------------------*)
(*対集合からシングルトンp1*)
Theorem SPairPrs1 : SPairf ->
 forall c x:Set, x /e {` c } -> x = c.
Proof.
 intros Hsp c x Hxc.
 cut ((x = c) \/ (x = c)).
 intro Hor.
 elim Hor.
 intro H; assumption.
 intro H; assumption.
 generalize Hxc.
 cut (x /e {`c} <-> x = c \/ x = c).
 intros (H1,H2); assumption.
 apply Hsp.
Qed.

Theorem SPairPrs2 : SPairf ->
 forall c x:Set, x = c -> x /e {` c }.
Proof.
 intros Hsp c x Hxc.
 assert (Hor:(x = c) \/ (x = c)).
 left; assumption.
 generalize Hor.
 cut (x /e {`c} <-> x = c \/ x = c).
 intros (H1,H2); assumption.
 apply Hsp.
Qed.

(*対集合からシングルトン*)
Theorem SPairPrs : SPairf ->
 forall c x:Set, x /e {` c } <-> x = c.
Proof.
 intros Hsp c x.
 split.
 apply SPairPrs1.
 exact Hsp.
 apply SPairPrs2.
 exact Hsp.
Qed.

(*-------------------------------------------------------------*)

Theorem SPairabc : SPairf ->
 forall a b c:Set,
 { a , b } = {` c } <-> a = c /\ b = c.
Proof.
 intros Hsp a b c.
 split.
 intro H.
 split.
 cut (a /e {` c }).
 cut (a /e {`c} <-> a = c).
 intros (H1,H2); assumption.
 apply SPairPrs.
 exact Hsp.
 rewrite <- H.
 apply SPairPrl.
 exact Hsp.
 cut (b /e {` c }).
 cut (b /e {`c} <-> b = c).
 intros (H1,H2); assumption.
 apply SPairPrs.
 exact Hsp.
 rewrite <- H.
 apply SPairPrr.
 exact Hsp.
 intros (Ha,Hb).
 rewrite Ha; rewrite Hb.
 reflexivity.
Qed.

Theorem SPairabcd : SPairf ->
 forall a b c d:Set,
 { a , b } = { c , d } -> a = c \/ a = d.
Proof.
 intros Hsp a b c d H.
 cut (a /e { c , d }).
 cut (a /e {c, d} <-> a = c \/ a = d).
 intros (H1,H2); assumption.
 apply Hsp.
 rewrite <- H.
 apply SPairPrl.
 exact Hsp.
Qed.

Theorem SPairnabcd : SPairf ->
 forall a b c d:Set,
 a <> c -> { a , b } = { c , d } -> a = d /\ b = c.
Proof.
 intros Hsp a b c d H1 H2.
 split.
 cut (a = c \/ a = d).
 intro cd.
 elim cd.
 intro ac.
 elim H1.
 assumption.
 intro ad; assumption.
 apply SPairabcd with (b := b).
 exact Hsp.
 assumption.
 symmetry.
 cut (c = a \/ c = b).
 intro ab.
 elim ab.
 intro ac.
 elim H1.
 symmetry.
 assumption.
 intro cb; assumption.
 apply SPairabcd with (b := d).
 exact Hsp.
 symmetry.
 assumption.
Qed.

Theorem SPairaabc : SPairf -> forall a b c:Set,
 { a , b } = { a , c } -> b = c.
Proof.
 intros Hsp a b c Hbc.
 assert (Hb:b = a \/ b = c).
 cut (b /e {a, c}).
 cut (b /e {a, c} <-> b = a \/ b = c).
 intros (H1,H2); assumption.
 apply Hsp.
 rewrite <- Hbc.
 apply SPairPrr.
 exact Hsp.
 elim Hb. (* Hb : b = a \/ b = cで場合わけ *)
 intro Hba. (*                                                 b = aからの証明 *)
 assert (Hc:c = a \/ c = b).
 cut (c /e {a, b}).
 cut (c /e {a, b} <-> c = a \/ c = b).
 intros (H1,H2); assumption.
 apply Hsp.
 rewrite Hbc.
 apply SPairPrr.
 exact Hsp.
 elim Hc. (* Hc : c = a \/ c = bで場合わけ *)
 intro Hca. (* c = aからの証明 *)
 transitivity a.
 assumption.
 symmetry.
 assumption.
 intro Hcb. (* c = bからの証明 *)
 symmetry.
 assumption.
 intro Hd. (*                                                b = cからの証明 *)
 assumption.
Qed.

SPairaabcの証明の主要部分

c∈{a,c}

[H:{a,b}={a,c}]

b∈{a,b}

[H:{a,b}={a,c}]

c∈{a,b}

[Hba:b=a]

[Hca:c=a]

[Hcb:c=b]

b∈{a,c}

c=a∨c=b

b=c

b=c

Hca,Hcb

b=a∨b=c

b=c

[Hbc:b=c]

Hba,Hbc

b=c

H

{a,b}={a,c}→b=c

(*順序対の基本性質1*)
Theorem SPairOrd1 : SPairf -> forall a b c d:Set,
 [ a , b ] = [ c , d ] -> (a = c /\ b = d).
Proof.
 intros Hsp a b c d.
 intro H.
 assert (Hac : a = c). (*                Hac : a = c *)
 cut ({` a } = {` c } \/ {` a } = { c , d }).
 intro H0.
 elim H0. (* ここからH0 : {`a} = {`c} \/ {`a} = {c, d}場合わけ *)
 intro H1. (* {`a} = {`c}から証明開始 *)
 cut (a /e {` c }).
 cut (a /e {` c } <-> a = c).
 intros (H2,H3); assumption.
 apply SPairPrs.
 exact Hsp.
 rewrite <- H1.
 apply SPairPrr.
 exact Hsp.
 intro H2. (* {`a} = {c, d}から証明開始 *)
 symmetry.
 cut (c = a /\ d = a).
 intros (H3,H4); assumption.
 cut ({ c , d } = {` a }).
 cut ({c, d} = {` a } <-> c = a /\ d = a).
 intros (H3,H4); assumption.
 apply SPairabc.
 exact Hsp.
 symmetry.
 assumption. (* {`a} = {c, d}からの証明終わり *)
 cut ({` a } /e [ c , d ]).
 cut ({` a } /e [ c, d ] <-> {` a } = {` c } \/ {` a } = { c , d }).
 intros (H3,H4); assumption.
 unfold SetOrP.
 apply Hsp.
 rewrite <- H.
 unfold SetOrP.
 apply SPairPrl.
 assumption.
 (* Hac : a = cの証明ここまで *)
 split.
 assumption.
 apply SPairaabc with a.
 assumption.
 apply SPairaabc with (a := {` a }).
 assumption.
 pattern a at 4; rewrite Hac.
 pattern a at 4; rewrite Hac.
 pattern a at 4; rewrite Hac.
 unfold SetOrP in H.
 exact H.
Qed.

SPairOrdの証明の主要部分

SPairOrd

{`a}∈[a,b]

[H:[a,b]=[c,d]]

a∈{`a}

[H1:{`a}={`c}]

c∈{c,d}

[H2:{`a}={c,d}]

{`a}∈[c,d]

a∈{`c}

c∈{`a}

{`a}={`c}∨{`a}={c,d}

a=c

a=c

H1,H2

[H:[a,b]=[c,d]]

[Hac:a=c]

[a,b]=[a,d]

{{`a},{a,b}}={{`a},{a,d}}

SPairaabc

{a,b}={a,d}

SPairaabc

[Hac:a=c]

b=d

a=c∧b=d

H

[a,b]=[c,d]→(a=c∧b=d)

(*順序対の基本性質2*)
Theorem SPairOrd2 : forall a b c d:Set,
 (a = c /\ b = d) -> ([ a , b ] = [ c , d ]).
Proof.
 intros a b c d.
 intros (Ha,Hb).
 rewrite Ha; rewrite Hb.
 reflexivity.
Qed.

(*順序対の基本性質2m*)
Theorem SPairOrd2m : forall a b c d:Set,
 (a = c) -> (b = d) -> ([ a , b ] = [ c , d ]).
Proof.
 intros a b c d.
 intros Ha Hb.
 rewrite Ha; rewrite Hb.
 reflexivity.
Qed.

(*順序対の基本性質*)
Theorem SPairOrd : SPairf -> forall a b c d:Set,
 [ a , b ] = [ c , d ] <-> a = c /\ b = d.
Proof.
 intros Hsp a b c d.
 split.
 apply SPairOrd1.
 exact Hsp.
 apply SPairOrd2.
Qed.

もどる