Library set_theory
Require Import Classical_Prop Classical_Pred_Type.
Require Import IndefiniteDescription ChoiceFacts.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import IndefiniteDescription ChoiceFacts.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
This file contains the set theory that will be used for the development
of topology. A set is represented by its characteristic proposition,
that is, a set of elements of type T has type T -> Prop.
If H has type {x : T | P x} then
pi1 H == x. It is a shortcut for proj1_sig.
pi2 H == a proof of P (pi1 H). It is a shortcut for proj2_sig.
If H has type exists x : T, P x then
cid H == an inhabitant of type {x : T | P x}. It is a
shortcut for constructive_indefinite_description.
Basic definitions
{ø : T} == the empty set over elements of type T. {full : T} == the set that contains all elements of type T. x 'in A == x is an element of the set A. (i.e., it is a proof of A x). A =s B == A is the same set of B. A <s B == the set A is included in the set B. A^c == the absolute complement of A. A \ B == the set A private of the elements of the set B. (it is the relative complement of B in A). inter A B == the intersection of A and B. union A B == the union of A and B. inter_s E F == if E is a set of sets (i.e., the type of E is (T -> Prop) -> Prop), it is the intersection of the sets F A such that A 'in E. union_s E F == if E is a set of sets (i.e., the type of E is (T -> Prop) -> Prop), it is the union of the sets F A such that A 'in E.Functions
image f == the set of y such that exists x, y = f x. f^(U) == the set of f x such that x 'in U. f^-1 y == the set of elements x such that y = f x. f@^-1 (U) == the union of f^-1 y such that y 'in U. inverse Hbf == if Hbf is a proof that f is bijective, it is the inverse function of f. The pretty printer uses the notation f-1.Family of sets
finite_set A == A is a finite set. family T Ti == the type of families of sets (of type T -> Prop) where Ti is the type of elements that indexes the family. (ind f) == the index of the family of sets f. finite_family == the type of finite family of sets. cardinality f == the number of sets in the family f. sub_family f g == the family of sets g is a subfamily of f. ind_seq f == a sequence of all indicies of finite family f. empty_fam f == f is an empty family of sets. fempty == the empty family of sets. inter_fam f == the intersection of all sets in the family f. union_fam f == the union of all sets in the family f. cover A f == the family of sets f covers the set A. fam_fin_to_seq f == a sequence that contains all sets of finite family f (it is of type seq (T -> Prop)). inter_seq s == the intersection of all sets in the sequence s. we define this to allows proof by induction in the case that we have finite number of sets.Set Implicit Arguments.
Import Prenex Implicits.
Notation pi1 := proj1_sig.
Notation pi2 := proj2_sig.
Notation cid := (constructive_indefinite_description _).
Section Teqtype.
Lemma cddo : forall T : Type, ConstructiveDefiniteDescription_on T.
Lemma eqProp : forall (P : Prop), {P} + {~P}.
Definition Propb (P : Prop) : bool:=
match (eqProp P) with
| left _ => true
| right _ => false
end.
Lemma Pb : forall (P : Prop), reflect P (Propb P).
Variable T : Type.
Definition eqT (x y : T) : bool := Propb (x = y).
Lemma eqTP : Equality.axiom eqT.
Canonical Structure T_eqMixin := Eval hnf in EqMixin eqTP.
End Teqtype.
Section prelemme.
Lemma orPC (A B : Prop) : (A \/ B) -> (B \/ A).
Lemma andPC (A B : Prop) : (A /\ B) <-> (B /\ A).
Lemma not_and_to_imply (A B : Prop) : ~(A /\ B) <-> (B -> ~A).
Lemma not_imply_to_and (A B : Prop) : ~(A -> B) <-> (A /\ ~ B).
End prelemme.
Section Ensemble.
Variable T : Type.
Require Export Setoid.
Require Export Morphisms.
Definition in_set (x : T) (A : T-> Prop) := A x.
Notation "x 'in A" := (in_set x A) (at level 3).
Lemma insE x (P : T -> Prop) : x 'in (fun x => P x) = P x.
Definition eqset (A B : T -> Prop) : Prop := forall x, x 'in A <-> x 'in B.
Notation "A =s B" := (eqset A B) (at level 70, no associativity).
Lemma eqset_refl : forall A, A =s A.
Lemma eqset_sym : forall A B, A =s B -> B =s A.
Lemma eqset_trans : forall A B C, A =s B -> B =s C -> A =s C.
Add Relation _ eqset
reflexivity proved by eqset_refl
symmetry proved by eqset_sym
transitivity proved by eqset_trans
as eqset_rel.
Add Parametric Morphism x : (in_set x)
with signature eqset ==> iff as in_set_mor.
Definition empty (x : T) : Prop := False.
Definition full (x : T) : Prop := True.
Definition include (A B : T -> Prop) := forall (x: T), x 'in A -> x 'in B.
Notation "A <s B" := (include A B) (at level 70, no associativity).
Add Morphism include with signature eqset ==> eqset ==> iff as include_mor.
Lemma include_trans A B C : A <s B -> B <s C -> A <s C.
Lemma left_i A B : A =s B -> A <s B.
Lemma right_i A B : A =s B -> B <s A.
Lemma double_i A B : A <s B -> B <s A -> A =s B.
Definition complementary (A : T -> Prop) x : Prop := ~ x 'in A.
Notation "A ^c" := (complementary A) (at level 2, no associativity).
Add Morphism complementary with signature eqset ==> eqset as compl_mor.
Lemma compl_invo A : (A^c)^c =s A.
Lemma compl_include A B : B^c <s A^c <-> A <s B.
Lemma empty_c : empty^c =s full.
Lemma full_c : full^c =s empty.
Lemma neq_compl A x y : x 'in A^c -> y 'in A -> x <> y.
Definition inter (A B: T -> Prop) x :Prop := x 'in A /\ x 'in B.
Add Morphism inter with signature eqset ==> eqset ==> eqset as inter_mor.
Lemma inter_sym A B : inter A B =s inter B A.
Lemma inter_neutr A B : A <s B -> inter A B =s A.
Lemma inter_left A B : inter A B <s A.
Lemma inter_right A B : inter A B <s B.
Lemma in_inter A B C D : A <s C -> B <s D -> inter A B <s inter C D.
Definition union (A B : T -> Prop) x := x 'in A \/ x 'in B.
Add Morphism union with signature eqset ==> eqset ==> eqset as union_mor.
Lemma union_sym A B : union A B =s union B A.
Lemma union_neutr A B : B <s A -> union A B =s A.
Lemma union_left A B : A <s union A B.
Lemma union_right A B : B <s union A B.
Lemma in_union A B C D : A <s C -> B <s D -> union A B <s union C D.
Lemma compl_inter A B : (inter A B)^c =s union A^c B^c.
Lemma compl_union A B : (union A B)^c =s inter A^c B^c.
Definition without (A B : T-> Prop) := inter A B^c.
Notation "A \ B" := (without A B) (at level 0, no associativity).
Add Morphism without with signature eqset ==> eqset ==> eqset as without_mor.
Lemma A_without_A A : A\A =s empty.
End Ensemble.
Notation "x 'in A" := (in_set x A) (at level 3).
Notation "A =s B" := (eqset A B) (at level 70, no associativity).
Notation "A <s B" := (include A B) (at level 70, no associativity).
Notation "A ^c" := (complementary A) (at level 2, no associativity).
Notation "A \ B" := (without A B) (at level 0, no associativity).
Notation "{ø : T }" := (@empty T).
Notation "{full : T }" := (@full T).
Add Parametric Morphism T : (@in_set (T -> Prop))
with signature (@eqset T) ==> ((@eqset T) ==> iff) ==> iff as in_setl_mor.
Section inter_union.
Variable T : Type.
Definition inter_s (E : (T -> Prop) -> Prop) (F : (T-> Prop) -> (T -> Prop))
(x : T) := forall A, A 'in E -> x 'in (F A) .
Definition union_s (E : (T -> Prop) -> Prop) (F : (T-> Prop) -> (T -> Prop))
(x : T) := exists A, A 'in E /\ x 'in (F A).
Lemma inters_in (E : (T -> Prop) -> Prop) F A :
A 'in E -> inter_s E F <s F A.
Lemma in_unions (E : (T -> Prop) -> Prop) F A :
A 'in E -> F A <s union_s E F.
Lemma inters_in2 E F A : A <s inter_s E F <-> forall S, S 'in E -> A <s F S.
Lemma in_unions2 E F A : union_s E F <s A <-> forall S, S 'in E -> F S <s A.
Lemma union_compl_inter E F :
(union_s E F)^c =s (inter_s E (fun A => (F A)^c)).
Lemma inter_compl_union E F :
(inter_s E F)^c =s (union_s E (fun A => (F A)^c)).
Lemma eq_union E F :
union_s E F =s union_s (fun B=> exists A, A 'in E /\ (F A =s B)) id.
Lemma eq_inter E F :
inter_s E F =s inter_s (fun B=> exists A, A 'in E /\ (F A =s B)) id.
Lemma eq_union2 E F E' F' : E =s E' -> (forall A, F A =s F' A) ->
union_s E F =s union_s E' F'.
Lemma eq_inter2 E F E' F' : E =s E' -> (forall A, F A =s F' A) ->
inter_s E F =s inter_s E' F'.
End inter_union.
Section function.
Variables T1 T2 T3 : Type.
Definition image (f : T1 -> T2) y := exists x, y = f x.
Definition range (f : T1 -> T2) (U : T1 -> Prop) (y : T2) :=
exists x, x 'in U /\ y = f x.
Notation "f ^( U )" := (range f U) (at level 0).
Add Parametric Morphism (f : T1 -> T2) :
(range f) with signature (@eqset T1) ==> (@eqset T2) as rng_mor.
Definition fiber (f : T1 -> T2) (y : T2) (x : T1) := y = f x.
Notation "f ^-1" := (fiber f).
Definition preimage (f : T1 -> T2) (U : T2 -> Prop) (x : T1) :=
exists y, y 'in U /\ x 'in (f^-1 y).
Notation "f @^-1( U )" := (preimage f U) (at level 0).
Add Parametric Morphism (f : T1 -> T2) :
(preimage f) with signature (@eqset T2) ==> (@eqset T1) as preim_mor.
Definition injective (f : T1 -> T2) := forall x y, f x = f y -> x = y.
Definition surjective (f : T1 -> T2) := forall (y : T2), exists x, y = f x.
Definition bijective (f : T1 -> T2) := injective f /\ surjective f.
Definition inverse f (Hbf : bijective f) := fun y => pi1 (cid ((proj2 Hbf) y)).
Lemma surj_eq : forall f, surjective f <-> f^({full : T1}) =s {full : T2}.
Lemma in_finv_f : forall (f : T1 -> T2) (U : T1 -> Prop), U <s f@^-1(f^(U)).
Lemma f_finv_in : forall (f : T1 -> T2) (U : T2 -> Prop), f^(f@^-1(U)) <s U.
Lemma surj_invo : forall f U, surjective f -> f^(f@^-1(U)) =s U.
Lemma inj_invo : forall f U, injective f -> f@^-1(f^(U)) =s U.
Lemma compl_finv : forall f U, f@^-1(U^c) =s f@^-1(U)^c.
Lemma compl_f_inj : forall f U, injective f -> f^(U^c) <s f^(U)^c.
Lemma compl_f_surj : forall f U, surjective f -> f^(U)^c <s f^(U^c).
Lemma compl_f_bij : forall f U, bijective f -> f^(U^c) =s f^(U)^c.
End function.
Notation "f ^( U )" := (range f U) (at level 0).
Notation "f ^-1" := (fiber f).
Notation "f @^-1( U )" := (preimage f U) (at level 0).
Notation "f '-1'" := (@inverse _ _ f _)(at level 30, format "f '-1'").
Section function2.
Variables T1 T2 T3 : Type.
Lemma comp_inv : forall (f : T1 -> T2) (g : T3 -> T1) U,
(f \o g)@^-1(U) =s g@^-1(f@^-1(U)).
End function2.
Section function3.
Variables T1 T2 T3 : Type.
Lemma left_id_rec : forall (f : T1 -> T2) (Hbf : bijective f) x,
((inverse Hbf) \o f) x = x.
Lemma right_id_rec : forall (f : T1 -> T2) (Hbf : bijective f) y,
(f \o (inverse Hbf)) y = y.
Lemma bij_rec : forall (f : T1 -> T2) (Hbf : bijective f),
bijective (inverse Hbf).
Lemma rec_invo : forall (f : T1 -> T2) (Hbf : bijective f) x,
inverse (bij_rec Hbf) x = f x.
End function3.
Section Family.
Variable T : Type.
Variable Ti : eqType.
Structure family : Type := mkfamily {
ind : Ti -> Prop;
F :> Ti -> T -> Prop
}.
Definition finite_set (T1 : eqType) (A : T1 -> Prop) :=
exists s : seq T1, A =s (fun x => x \in s).
Structure finite_family := Ff {
fam :> family;
_ : finite_set (ind fam)
}.
Lemma finfam : forall (f : finite_family), finite_set (ind f).
Definition ind_seq (f : finite_family) := pi1 (cid (finfam f)).
Lemma ind_seqP (f : finite_family) : (ind f) =s (fun x => x \in (ind_seq f)).
Definition inter_fam (f : family) (x : T) :=
forall i, i 'in (ind f) -> x 'in (f i) .
Definition union_fam (f : family) (x : T) :=
exists i, i 'in (ind f) /\ x 'in (f i).
Definition cover (A : T -> Prop) (f : family) := A <s union_fam f.
Definition sub_family f g :=
ind g <s ind f /\ forall i, i 'in (ind g) -> f i =s g i.
Definition empty_fam (f : family) := ind f <s {ø : Ti}.
Lemma fam_empty (f : family) : (forall x : Ti, x 'in {ø : Ti}) -> empty_fam f.
Lemma union_empty (f : family) : empty_fam f -> union_fam f =s {ø : T}.
Lemma inter_empty (f : family) : empty_fam f -> inter_fam f =s {full : T}.
Lemma in_union_fam (f : family) i : i 'in (ind f) -> f i <s union_fam f.
Lemma inter_fam_in (f : family) i : i 'in (ind f) -> inter_fam f <s f i.
Definition cardinality (f : finite_family) := size (ind_seq f).
Lemma fempty_def f : empty_fam f -> finite_set (ind f).
Definition fempty f (Hf : empty_fam f) := Ff (fempty_def Hf).
Definition fam_fin_to_seq (f : finite_family) := map f (ind_seq f).
Lemma fam_card (f : finite_family) : size (fam_fin_to_seq f) = cardinality f.
Lemma fam_fin_v (f : finite_family) :
(fam_fin_to_seq f) = [::] <-> empty_fam f.
Lemma card_empty f (H : empty_fam f) : cardinality (fempty H) = 0.
Canonical set_eqType := Eval hnf in EqType (T -> Prop) (T_eqMixin (T -> Prop)).
Lemma fam_fin_eq (f : finite_family) (g : T -> Prop) :
g \in (fam_fin_to_seq f) <-> exists i : Ti, i 'in (ind f) /\ g = f i.
Definition inter_seq (s : seq (T -> Prop)) :=
foldr (@inter T) {full : T} s.
Definition inter_fam_fin (f : finite_family) :=
inter_seq (fam_fin_to_seq f).
Lemma in_inter_seq : forall (s : seq (T -> Prop)) g, g \in s ->
inter_seq s <s g.
Lemma in_inter_seq2 : forall (s : seq (T -> Prop)) x,
(forall g, g \in s -> x 'in g) -> x 'in (inter_seq s).
Lemma inter_fin_eq (f : finite_family) : inter_fam f =s inter_fam_fin f.
End Family.
This page has been generated by coqdoc