From 6c49bf832dd39cb170f6bcdbc6940e2e81abc650 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 8 Sep 2008 13:49:15 +0000 Subject: [PATCH] ... --- .../formal_topology/concrete_spaces.ma | 75 +++++++++++++------ 1 file changed, 51 insertions(+), 24 deletions(-) diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma index 5c39bedde..703facfa5 100644 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -93,51 +93,65 @@ record concrete_space : Type ≝ all_covered: ∀x: concr bp. x ⊩ form bp }. -(* record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ { rp:> relation_pair CS1 CS2; respects_converges: ∀b,c. - extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) = - extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c)); + extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) = + BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c)); respects_all_covered: - extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) = - extS ?? (rel CS1) (form CS1) + extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1) }. -definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid. +definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. intros; constructor 1; [ apply (convergent_relation_pair c c1) | constructor 1; [ intros; apply (relation_pair_equality c c1 c2 c3); - | intros 1; apply refl; - | intros 2; apply sym; - | intros 3; apply trans]] + | intros 1; apply refl1; + | intros 2; apply sym1; + | intros 3; apply trans1]] qed. -lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X. +lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. intros; - unfold extS; - split; - [ intros 2; - cases m; clear m; + unfold extS; simplify; + split; simplify; + [ intros 2; change with (a ∈ X); + cases f; clear f; cases H; clear H; - cases H1; clear H1; - whd in H; - apply (eq_elim_r'' ????? H); + cases x; clear x; + change in f2 with (eq1 ? a w); + apply (. (f2\sup -1‡#)); assumption - | intros 2; - constructor 1; + | intros 2; change in f with (a ∈ X); + split; [ whd; exact I | exists; [ apply a ] split; [ assumption - | whd; constructor 1]]] + | change with (a = a); apply refl]]] qed. -definition CSPA: category. +lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X. + intros; + unfold extS; simplify; + split; simplify; intros; + [ change with (a ∈ X); + cases f; cases H; cases x; change in f3 with (eq1 ? a w); + apply (. (f3\sup -1‡#)); + assumption + | change in f with (a ∈ X); + split; + [ apply I + | exists; [apply a] + split; [ assumption | change with (a = a); apply refl]]] +qed. + +(* +definition CSPA: category1. constructor 1; [ apply concrete_space | apply convergent_relation_space_setoid @@ -146,7 +160,20 @@ definition CSPA: category. | intros; unfold id; simplify; apply (.= (equalset_extS_id_X_X ??)); - - | + apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡ + (equalset_extS_id_X_X ??)\sup -1))); + apply refl1; + | apply (.= (extS_id ??)); + apply refl1] + | intros; constructor 1; + [ intros; whd in c c1 ⊢ %; + constructor 1; + [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] + | intros; + | + ] + | intros; intros 2; simplify; + letin xxx ≝ (comp BP); clearbody xxx; unfold BP in xxx:(?→?→?→?→?→%); simplify in xxx; + unfold basic_pair in xxx; simplify in xxx; ] - |*) \ No newline at end of file +*) \ No newline at end of file -- 2.39.2