ページが重すぎるので分割します。
前編
https://qiita.com/Meizen_OS/items/30cd4fb59ade0b94276e
Section Power_Relation_Mapping.
(*冪集合のwell-defined*)
Theorem WDPow:forall x:Set, exists! p, forall y:Set, In y p <-> Sbs y x.
Proof.
intro.
apply WDSetIffU.
specialize (AxPower x).
intro.
destruct H.
exists x0.
apply H.
Qed.
(*冪集合*)
Axiom Pow:Set -> Set.
Axiom AxPow:forall x y:Set, In y (Pow x) <-> Sbs y x.
(*{z⊆X|P(z)}の存在*)
Theorem ExPowIff:forall (P:Set -> Prop) (X:Set),
exists S, forall z:Set, In z S <-> Sbs z X /\ P z.
Proof.
intros.
apply ExSetIff.
specialize (AxPower X).
intro.
destruct H.
exists x.
intros.
apply H.
apply H0.
Qed.
(*外延、分出、対、和集合、冪 -> 直積のwell-defined*)
Theorem WDTimes:forall a b:Set, exists! t, forall z:Set,
In z t <-> exists x y, In x a /\ In y b /\ z=OP x y.
Proof.
intros.
apply WDSetIffU.
exists (Pow (Pow (Cup a b))).
intros.
apply AxPow.
intro.
intro.
apply AxPow.
intro.
intro.
apply AxCup.
destruct H.
destruct H.
destruct H.
destruct H2.
rewrite H3 in H0.
apply AxPR in H0.
destruct H0.
rewrite H0 in H1.
apply AxSngl in H1.
left.
rewrite H1.
apply H.
rewrite H0 in H1.
apply AxPR in H1.
destruct H1.
left.
rewrite H1.
apply H.
right.
rewrite H1.
apply H2.
Qed.
(*直積集合*)
Axiom Times:Set -> Set -> Set.
Axiom AxTimes:forall a b z:Set,
In z (Times a b) <-> exists x y, In x a /\ In y b /\ z=OP x y.
(*∀x∀y((x,y)∈a×b⇔x∈a∧y∈b)*)
Theorem TimesIff:forall a b x y:Set,
In (OP x y) (Times a b) <-> In x a /\ In y b.
Proof.
split.
intro.
apply AxTimes in H.
destruct H.
destruct H.
destruct H.
destruct H0.
apply OPC in H1.
destruct H1.
split.
rewrite H1.
apply H.
rewrite H2.
apply H0.
intros.
destruct H.
apply AxTimes.
exists x.
exists y.
split.
apply H.
split.
apply H0.
reflexivity.
Qed.
(*重要*)
(*{(x,y)|x∈X∧y∈Y∧P(x,y)}の存在*)
Theorem ExRelIff:forall (P:Set -> Set -> Prop) (X Y:Set), exists R,
forall z:Set, In z R <-> exists x y, In x X /\ In y Y /\ z = OP x y /\ P x y.
Proof.
intros.
apply ExSetIff.
exists (Times X Y).
intros.
destruct H.
destruct H.
destruct H.
destruct H0.
destruct H1.
rewrite H1.
apply TimesIff.
split.
apply H.
apply H0.
Qed.
(*二項関係の略記xRy:⇔(x,y)∈R*)
Definition REL(R x y:Set):= In (OP x y) R.
(*二項関係*)
Definition Rel(R X Y:Set):=
forall z:Set, In z R -> exists x y, In x X /\ In y Y /\ z= OP x y.
(*X,Y上の二項関係ならばxRy⇒x∈X∧y∈Y*)
Theorem RelIn:forall R X Y x y:Set, Rel R X Y ->
In (OP x y) R -> In x X /\ In y Y.
Proof.
intros.
apply H in H0.
destruct H0.
destruct H0.
destruct H0.
destruct H1.
apply OPC in H2.
destruct H2.
split.
rewrite H2.
apply H0.
rewrite H3.
apply H1.
Qed.
(*∀x∈X ∀y∈Y (xRy⇔P(x,y))となるX,Y上の二項関係のwell-defined*)
Theorem WDRel:forall (P:Set -> Set -> Prop) (X Y:Set),
exists!R, Rel R X Y /\
forall x y:Set, In x X -> In y Y -> (REL R x y <-> P x y).
Proof.
intros.
specialize (ExRelIff P X Y).
intros.
destruct H.
exists x.
split.
split.
intro.
intro.
apply H in H0.
destruct H0.
destruct H0.
exists x0.
exists x1.
split.
apply H0.
split.
apply H0.
apply H0.
split.
intro.
apply H in H2.
destruct H2.
destruct H2.
destruct H2.
destruct H3.
destruct H4.
apply OPC in H4.
destruct H4.
rewrite H4.
rewrite H6.
apply H5.
intro.
apply H.
exists x0.
exists y.
split.
apply H0.
split.
apply H1.
split.
reflexivity.
apply H2.
intros.
apply AxEx.
destruct H0.
split.
intro.
apply H in H2.
destruct H2.
destruct H2.
destruct H2.
destruct H3.
destruct H4.
rewrite H4.
specialize (H1 x0 x1 H2 H3).
apply H1 in H5.
apply H5.
intro.
apply H.
specialize (H0 z H2).
destruct H0.
destruct H0.
exists x0.
exists x1.
split.
apply H0.
split.
apply H0.
split.
apply H0.
apply H1.
apply H0.
apply H0.
destruct H0.
destruct H3.
rewrite H4 in H2.
apply H2.
Qed.
(*半順序*)
Definition Poset(X R:Set):=
(forall z:Set, In z R -> exists x y, In x X /\ In y X /\ z = OP x y) /\
(forall x:Set, In x X -> REL R x x) /\
(forall x y z:Set, REL R x y -> REL R y z -> REL R x z) /\
(forall x y:Set, REL R x y -> REL R y x -> x = y).
(*部分集合を集合に制限して二項関係として扱っていいことのwell-defined*)
Theorem WDRelSbs:forall X:Set,
exists!R, Rel R X X /\
forall x y:Set, In x X -> In y X -> (REL R x y <-> Sbs x y).
Proof.
intros.
apply (WDRel Sbs X X).
Qed.
(*部分集合を集合に制限して二項関係として扱ってよい*)
Axiom RelSbs:Set -> Set.
Axiom AxRelSbs: forall X:Set,
Rel (RelSbs X) X X /\
forall x y:Set, In x X -> In y X -> (REL (RelSbs X) x y <-> Sbs x y).
(*部分集合を制限して二項関係にすると半順序になる*)
Theorem RelSbsPoset:forall X:Set, Poset X (RelSbs X).
Proof.
intro.
specialize (AxRelSbs X).
intro.
destruct H.
split.
apply H.
split.
intros.
apply (H0 x x H1 H1).
apply RefSbs.
split.
intros.
specialize (RelIn ((RelSbs X)) X X x y H H1).
intros.
destruct H3.
specialize (RelIn ((RelSbs X)) X X y z H H2).
intros.
destruct H5.
apply (H0 x z H3 H6).
apply (H0 x y H3 H4) in H1.
apply (H0 y z H4 H6) in H2.
apply (TraSbs x y z H1 H2).
intros.
specialize (RelIn ((RelSbs X)) X X x y H H1).
intros.
destruct H3.
apply (H0 x y H3 H4) in H1.
apply (H0 y x H4 H3) in H2.
apply (AnSySbs x y H1 H2).
Qed.
(*値*)
Axiom VL:Set -> Set -> Set.
Axiom AxVL:forall f x:Set, (exists! y, In (OP x y) f) -> In (OP x (VL f x)) f.
(*写像*)
Definition To(f X Y:Set):=
(forall z:Set, In z f -> exists x y, In x X /\ In y Y /\ z= OP x y) /\
forall x:Set, In x X -> exists! y, In (OP x y) f.
(*写像は二項関係*)
Theorem ToImpRel:forall f X Y:Set, To f X Y -> Rel f X Y.
Proof.
intros.
destruct H.
intro.
apply H.
Qed.
(*f⊆X×Y*)
Theorem ToRel:forall f X Y x y:Set, To f X Y -> In (OP x y) f -> In x X /\ In y Y.
Proof.
intros.
apply ToImpRel in H.
apply (RelIn f X Y x y H H0).
Qed.
(*写像はグラフで定義されている*)
Theorem ToVLOP:forall f X Y x:Set, To f X Y -> In x X -> In (OP x (VL f x)) f.
Proof.
intros.
apply AxVL.
destruct H.
apply (H1 x H0).
Qed.
(*f:X→Y⇒(x,y)∈f⇔x∈X∧y=f(x)*)
Theorem ToVLIff:forall f X Y x y:Set, To f X Y ->
(In (OP x y) f <-> In x X /\ y = VL f x).
Proof.
split.
intro.
specialize (ToRel f X Y x y H H0).
intro.
destruct H1.
specialize (ToVLOP f X Y x H H1).
intro.
split.
apply H1.
destruct H.
specialize (H4 x H1).
apply (Uni (fun y => In (OP x y) f) H4 y (VL f x) H0 H3).
intro.
destruct H0.
rewrite H1.
apply (ToVLOP f X Y x H H0).
Qed.
(*定義域の元は終域に写る*)
Theorem ToVL:forall f X Y x:Set, To f X Y -> In x X -> In (VL f x) Y.
Proof.
intros.
apply (ToVLOP f X Y x H) in H0.
apply (ToRel f X Y x (VL f x) H) in H0.
apply H0.
Qed.
(*一点からの写像*)
Theorem SnglTo:forall a x X:Set,
In x X -> To (Sngl (OP a x)) (Sngl a) X.
Proof.
split.
intros.
apply AxSngl in H0.
exists a.
exists x.
split.
apply InSngl.
split.
apply H.
apply H0.
intros.
exists x.
apply AxSngl in H0.
rewrite H0.
split.
apply InSngl.
intros.
apply AxSngl in H1.
apply OPC in H1.
symmetry.
apply H1.
Qed.
(*一点からの写像の値*)
Theorem SnglToVL:forall a x:Set, VL (Sngl (OP a x)) a = x.
Proof.
intros.
specialize (InSngl x).
intro.
specialize (SnglTo a x (Sngl x) H).
specialize (InSngl a).
intros.
specialize (ToVLOP (Sngl (OP a x)) (Sngl a) (Sngl x) a H1 H0).
intro.
apply AxSngl in H2.
apply OPC in H2.
apply H2.
Qed.
(*写像の和集合*)
Theorem ToCup:forall f X Y g W Z:Set, To f X Y -> To g W Z ->
(forall x:Set, In x X -> In x W -> VL f x = VL g x) ->
To (Cup f g) (Cup X W) (Cup Y Z).
Proof.
intros.
split.
intros.
apply AxCup in H2.
destruct H2.
destruct H.
specialize (H z H2).
destruct H.
destruct H.
destruct H.
destruct H4.
exists x.
exists x0.
split.
apply AxCup.
left.
apply H.
split.
apply AxCup.
left.
apply H4.
apply H5.
destruct H0.
specialize (H0 z H2).
destruct H0.
destruct H0.
destruct H0.
destruct H4.
exists x.
exists x0.
split.
apply AxCup.
right.
apply H0.
split.
apply AxCup.
right.
apply H4.
apply H5.
intros.
apply AxCup in H2.
destruct H2.
exists (VL f x).
split.
apply AxCup.
left.
apply (ToVLOP f X Y x H H2).
intros.
apply AxCup in H3.
symmetry.
destruct H3.
apply (ToVLIff f X Y x x' H) in H3.
apply H3.
specialize (ToRel g W Z x x' H0 H3).
intro.
destruct H4.
rewrite (H1 x H2 H4).
apply (ToVLIff g W Z x x' H0) in H3.
apply H3.
exists (VL g x).
split.
apply AxCup.
right.
apply (ToVLOP g W Z x H0 H2).
intros.
apply AxCup in H3.
symmetry.
destruct H3.
specialize (ToRel f X Y x x' H H3).
intro.
destruct H4.
rewrite <- (H1 x H4 H2).
apply (ToVLIff f X Y x x' H) in H3.
apply H3.
apply (ToVLIff g W Z x x' H0) in H3.
apply H3.
Qed.
(*写像の和集合の値*)
Theorem ToCupVLL:forall f X Y g W Z:Set, To f X Y -> To g W Z ->
(forall x:Set, In x X -> In x W -> VL f x = VL g x) ->
forall x:Set, In x X -> VL (Cup f g) x = VL f x.
Proof.
intros.
apply (ToCup f X Y g W Z H H0) in H1.
apply (ToVLOP f X Y x H) in H2.
apply (SbsCupL f g) in H2.
apply (ToVLIff (Cup f g) (Cup X W) (Cup Y Z) x (VL f x) H1) in H2.
symmetry.
apply H2.
Qed.
(*写像の和集合の値*)
Theorem ToCupVLR:forall f X Y g W Z:Set, To f X Y -> To g W Z ->
(forall x:Set, In x X -> In x W -> VL f x = VL g x) ->
forall x:Set, In x W -> VL (Cup f g) x = VL g x.
Proof.
intros.
apply (ToCup f X Y g W Z H H0) in H1.
apply (ToVLOP g W Z x H0) in H2.
apply (SbsCupR f g) in H2.
apply (ToVLIff (Cup f g) (Cup X W) (Cup Y Z) x (VL g x) H1) in H2.
symmetry.
apply H2.
Qed.
(*外延、分出、直積->写像の存在*)
Theorem WDTo:forall P:Set -> Set -> Prop, forall X Y:Set,
(forall x:Set, In x X -> exists!y:Set, In y Y /\ P x y)
-> exists f, To f X Y /\ forall x:Set, In x X -> P x (VL f x).
Proof.
intros.
specialize (ExRelIff P X Y).
intro.
destruct H0.
exists x.
cut (To x X Y).
intro.
split.
apply H1.
intros.
specialize (H x0 H2).
apply (ToVLOP x X Y x0 H1) in H2.
apply H0 in H2.
destruct H2.
destruct H2.
destruct H2.
destruct H3.
destruct H4.
apply OPC in H4.
destruct H4.
rewrite H6.
rewrite H4.
apply H5.
split.
intros.
apply H0 in H1.
destruct H1.
destruct H1.
exists x0.
exists x1.
split.
apply H1.
split.
apply H1.
apply H1.
intros.
specialize (H x0 H1).
destruct H.
destruct H.
destruct H.
exists x1.
split.
apply H0.
exists x0.
exists x1.
split.
apply H1.
split.
apply H.
split.
reflexivity.
apply H3.
intros.
apply H0 in H4.
destruct H4.
destruct H4.
destruct H4.
destruct H5.
destruct H6.
apply OPC in H6.
apply H2.
destruct H6.
rewrite H6.
rewrite H8.
split.
apply H5.
apply H7.
Qed.
Section Power_Relation_Mapping.