From 05669a3646cbf8219bf772718b4b2c5bfd1ddd82 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Jan 2009 09:08:09 +0000 Subject: [PATCH] Just a snapshot. --- .../formal_topology/overlap/o-basic_pairs.ma | 16 ++++ .../o-basic_pairs_to_o-basic_topologies.ma | 83 +++++++++++++++++++ .../overlap/o-concrete_spaces.ma | 18 +--- 3 files changed, 100 insertions(+), 17 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 7e0064e46..956a26af9 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -185,3 +185,19 @@ qed. interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y). interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). *) + +notation "□ \sub b" non associative with precedence 90 for @{'box $b}. +notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}. +interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)). + +notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}. +notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}. +interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)). + +notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}. +notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}. +interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)). + +notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}. +notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}. +interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)). diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma new file mode 100644 index 000000000..324e51df7 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "o-basic_pairs.ma". +include "o-basic_topologies.ma". + +lemma pippo: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r. + intros; + cut (r = binary_meet ? r r); (* la notazione non va ??? *) + [ apply (. (#‡Hcut) ^ -1); + apply oa_overlap_preservers_meet; + | + ] + +(* Part of proposition 9.9 *) +lemma lemmax: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R p ≤ R q. + intros; + apply oa_density; intros; + apply (. (or_prop3 : ?) ^ -1); + apply + +(* Lemma 10.2, to be moved to OA *) +lemma lemma_10_2_a: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R⎻* (R⎻ p). + intros; + apply (. (or_prop2 : ?)); + apply oa_leq_refl. +qed. + +lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p. + intros; + apply (. (or_prop2 : ?) ^ -1); + apply oa_leq_refl. +qed. + +lemma lemma_10_3: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p. + intros; apply oa_leq_antisym; + [ lapply (lemma_10_2_b ?? R p); + + | apply lemma_10_2_a;] +qed. + + + +(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) +definition o_basic_topology_of_basic_pair: BP → BTop. + intro; + constructor 1; + [ apply (form t); + | apply (□_t ∘ Ext⎽t); + | apply (◊_t ∘ Rest⎽t); + | intros 2; + lapply depth=0 (or_prop1 ?? (rel t)); + lapply depth=0 (or_prop2 ?? (rel t)); + + | + | + ] +qed. + +definition o_convergent_relation_pair_of_convergent_relation_pair: + ∀BP1,BP2.cic:/matita/formal_topology/concrete_spaces/convergent_relation_pair.ind#xpointer(1/1) BP1 BP2 → + convergent_relation_pair (o_concrete_space_of_concrete_space BP1) (o_concrete_space_of_concrete_space BP2). + intros; + constructor 1; + [ apply (orelation_of_relation ?? (r \sub \c)); + | apply (orelation_of_relation ?? (r \sub \f)); + | lapply (commute ?? r); + lapply (orelation_of_relation_preserves_equality ???? Hletin); + apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1); + apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r))); + apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index e90ec7fe4..57ec577ae 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -15,22 +15,6 @@ include "o-basic_pairs.ma". include "o-saturations.ma". -notation "□ \sub b" non associative with precedence 90 for @{'box $b}. -notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}. -interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)). - -notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}. -notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}. -interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)). - -notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}. -notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}. -interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)). - -notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}. -notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}. -interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)). - definition A : ∀b:BP. unary_morphism1 (form b) (form b). intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); @@ -161,4 +145,4 @@ definition CSPA: category2. | intros; simplify; change with (id2 ? o2 ∘ a = a); apply (id_neutral_left2 : ?);] -qed. \ No newline at end of file +qed. -- 2.39.2