X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations.ma;h=eda2cfc6d7550bfb813ad667739d736d4eb77668;hb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;hp=5678b6a892bbc75c2f5f97852dd3c820566349e5;hpb=7db606e36d5c17681a62cf5186bafde65cbfa3db;p=helm.git diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index 5678b6a89..eda2cfc6d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -19,9 +19,9 @@ record binary_relation (A,B: SET) : Type1 ≝ notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}. notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. -interpretation "relation applied" 'satisfy r x y = (fun21 ___ (satisfy __ r) x y). +interpretation "relation applied" 'satisfy r x y = (fun21 ??? (satisfy ?? r) x y). -definition binary_relation_setoid: SET → SET → SET1. +definition binary_relation_setoid: SET → SET → setoid1. intros (A B); constructor 1; [ apply (binary_relation A B) @@ -36,9 +36,13 @@ definition binary_relation_setoid: SET → SET → SET1. assumption]] qed. +definition binary_relation_of_binary_relation_setoid : + ∀A,B.binary_relation_setoid A B → binary_relation A B ≝ λA,B,c.c. +coercion binary_relation_of_binary_relation_setoid. + definition composition: ∀A,B,C. - binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C). + (binary_relation_setoid A B) × (binary_relation_setoid B C) ⇒_1 (binary_relation_setoid A C). intros; constructor 1; [ intros (R12 R23); @@ -94,34 +98,31 @@ definition REL: category1. first [apply refl | assumption]]] qed. -definition full_subset: ∀s:REL. Ω \sup s. +definition setoid_of_REL : objs1 REL → setoid ≝ λx.x. +coercion setoid_of_REL. + +definition binary_relation_setoid_of_arrow1_REL : + ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x. +coercion binary_relation_setoid_of_arrow1_REL. + +definition full_subset: ∀s:REL. Ω^s. apply (λs.{x | True}); intros; simplify; split; intro; assumption. qed. coercion full_subset. -definition setoid1_of_REL: REL → setoid ≝ λS. S. -coercion setoid1_of_REL. - -lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*). - [ apply rule o1; - | intros; apply t;] -qed. -coercion Type_OF_setoid1_of_REL. - -definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b. - apply (λb:REL. λP: b ⇒ CPROP. {x | P x}); +alias symbol "arrows1_SET" (instance 2) = "'arrows1_SET low". +definition comprehension: ∀b:REL. (b ⇒_1 CPROP) → Ω^b. + apply (λb:REL. λP: b ⇒_1 CPROP. {x | P x}); intros; simplify; - alias symbol "trans" = "trans1". - alias symbol "prop1" = "prop11". apply (.= †e); apply refl1. qed. interpretation "subset comprehension" 'comprehension s p = - (comprehension s (mk_unary_morphism1 __ p _)). + (comprehension s (mk_unary_morphism1 ?? p ?)). -definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X). +definition ext: ∀X,S:REL. (arrows1 ? X S) × S ⇒_1 (Ω^X). apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?); [ intros; simplify; apply (.= (e‡#)); apply refl1 | intros; simplify; split; intros; simplify; @@ -183,7 +184,7 @@ qed. *) (* the same as ⋄ for a basic pair *) -definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). +definition image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V. intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S }); intros; simplify; split; intro; cases e1; exists [1,3: apply w] @@ -197,7 +198,7 @@ definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \ qed. (* the same as □ for a basic pair *) -definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). +definition minus_star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V. intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S}); intros; simplify; split; intros; apply f; @@ -208,7 +209,7 @@ definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \s qed. (* the same as Rest for a basic pair *) -definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U). +definition star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U. intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S}); intros; simplify; split; intros; apply f; @@ -219,7 +220,7 @@ definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) qed. (* the same as Ext for a basic pair *) -definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U). +definition minus_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U. intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*) exT ? (λy:V.x ♮r y ∧ y ∈ S) });