微分トポロジー１５ 〜過去・現在・未来〜 2015/3/27 （久我）
位相空間論を形式化し（はじめ）よう!
最初の練習：ヒルベルトの公理S
Require Import ssreflect ssrbool.
Set Implicit Arguments.
Section HilbertS.
Variables A B C : Prop.
Lemma HilbertS : (A → B → C) → (A → B) → A → C.
Proof.
move⇒ H_AiBiC H_AiB H_A.
apply H_AiBiC.
assumption.
apply H_AiB.
assumption.
Qed.
End HilbertS.
集合 (Ensembles)
Section Ensembles.
Variable U : Type.
Definition Ensemble := U → Prop.
Definition In (A : Ensemble) (x : U) := A x.
空集合、全体集合
Inductive Empty_set : Ensemble :=.
Lemma Empty_set_is_empty :
∀ x : U, ¬ (In Empty_set x).
Proof.
move⇒ x H.
red in H.
SearchAbout Empty_set.
pose P := fun (x : U) ⇒ False.
have HF: (P x) = False.
by [].
rewrite<-HF.
by apply Empty_set_ind.
Qed.
Inductive Full_set : Ensemble :=
Full_intro : ∀ x : U, In Full_set x.
和集合、共通部分
Inductive Union (A B : Ensemble) : Ensemble :=
| Union_introl : ∀ x : U, In A x → In (Union A B) x
| Union_intror : ∀ x : U, In B x → In (Union A B) x.
Inductive Intersection (A B : Ensemble) : Ensemble :=
Intersection_intro : ∀ x : U,
In A x → In B x → In (Intersection A B) x.
包含関係、等号
Definition Included (A B : Ensemble) : Prop:=
∀ x : U, In A x → In B x.
Definition Same_set (A B : Ensemble) : Prop :=
Included A B ∧ Included B A.
外延性公理
Axiom Extensionality_Ensembles :
∀ A B : Ensemble, Same_set A B → A = B.
End Ensembles.
Section Families.
集合族 (Family)
Variable U : Type.
Definition Family := Ensemble (Ensemble U).
Variable F : Family.
Inductive FamilyUnion : Ensemble U :=
family_union_intro : ∀ (x : U) (S : Ensemble U),
In S x → In F S → In FamilyUnion x.
End Families.
位相空間の公理
Set Implicit Arguments.
Section TopologyAxioms.
Record TopologicalSpace : Type := {
point_set : Type;
open : Ensemble point_set → Prop;
open_family_union : ∀ F : Family point_set,
(∀ S : Ensemble point_set, In F S → open S) →
open (FamilyUnion F);
open_intersection2: ∀ U V:Ensemble point_set,
open U → open V → open (Intersection U V);
open_full : open (@Full_set _)
}.
定理 空集合は開集合
Lemma empty_family_union: ∀ U : Type,
FamilyUnion (@Empty_set (Ensemble U)) = @Empty_set _.
Proof.
move ⇒ U.
apply Extensionality_Ensembles.
rewrite/Same_set.
rewrite/Included.
apply conj.
move⇒x H.
destruct H.
contradiction.
move⇒x H.
by destruct H.
Qed.
Theorem open_empty: ∀ X:TopologicalSpace,
open _ (@Empty_set (point_set X)).
Proof.
intros.
rewrite <- empty_family_union.
apply open_family_union.
intros.
destruct H.
Qed.
End TopologyAxioms.