From 33f71ba86f8bbee8d5318b2cb3a96e890620aaba Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Sep 2008 09:17:02 +0000 Subject: [PATCH] Precedence level of \downarrow changed to match that of the binary one. --- helm/software/matita/core_notation.moo | 4 ++- .../formal_topology/formal_topologies.ma | 32 +++++++++++++++++-- 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index c6f66918d..025a9899d 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -201,7 +201,9 @@ notation "hvbox(a break \circ b)" left associative with precedence 55 for @{ 'compose $a $b }. -notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }. +notation "↓a" with precedence 55 for @{ 'downarrow $a }. + +notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}. notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }. diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma index 2acb5642d..62b11676a 100644 --- a/helm/software/matita/library/formal_topology/formal_topologies.ma +++ b/helm/software/matita/library/formal_topology/formal_topologies.ma @@ -59,7 +59,35 @@ qed. interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V). record formal_map (S,T: formal_topology) : Type ≝ - { cr:> continuous_relation S T; + { cr:> continuous_relation_setoid S T; C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c); C2: extS ?? cr T = S - }. \ No newline at end of file + }. + +definition formal_map_setoid: formal_topology → formal_topology → setoid1. + intros (S T); constructor 1; + [ apply (formal_map S T); + | constructor 1; + [ apply (λf,f1: formal_map S T.f=f1); + | simplify; intros 1; apply refl1 + | simplify; intros 2; apply sym1 + | simplify; intros 3; apply trans1]] +qed. + +definition cr': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝ + λFT1,FT2,c.cr ?? c. + +coercion cr'. + +(* +definition formal_map_composition: + ∀o1,o2,o3: formal_topology. + binary_morphism1 + (formal_map_setoid o1 o2) + (formal_map_setoid o2 o3) + (formal_map_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1; constructor 1; + [ apply (comp1 BTop ??? c c1); + | intros; +*) \ No newline at end of file -- 2.39.2