1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval".
21 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
23 include "ftc/IntervalFunct.ma".
31 In this file we prove that there are mappings going in both ways
32 between the set of partial functions whose domain contains
33 [[a,b]] and the set of real-valued functions with domain on
34 that interval. These mappings form an adjunction, and thus they have
35 all the good properties for preservation results.
39 We begin by defining the map from partial functions to setoid
40 functions as simply being the restriction of the partial function to
43 %\begin{convention}% Let [F] be a partial function and [a,b:IR] such
44 that [I [=] [a,b]] is included in the domain of [F].
48 inline "cic:/CoRN/ftc/PartInterval/F.var".
50 inline "cic:/CoRN/ftc/PartInterval/a.var".
52 inline "cic:/CoRN/ftc/PartInterval/b.var".
54 inline "cic:/CoRN/ftc/PartInterval/Hab.var".
58 inline "cic:/CoRN/ftc/PartInterval/I.con".
62 inline "cic:/CoRN/ftc/PartInterval/Hf.var".
64 inline "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
66 inline "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
73 Implicit Arguments IntPartIR [F a b Hab].
77 Section AntiConversion.
81 To go the other way around, we simply take a setoid function [f] with
82 domain [[a,b]] and build the corresponding partial function.
85 inline "cic:/CoRN/ftc/PartInterval/a.var".
87 inline "cic:/CoRN/ftc/PartInterval/b.var".
89 inline "cic:/CoRN/ftc/PartInterval/Hab.var".
93 inline "cic:/CoRN/ftc/PartInterval/I.con".
97 inline "cic:/CoRN/ftc/PartInterval/f.var".
99 inline "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
101 inline "cic:/CoRN/ftc/PartInterval/PartInt.con".
108 Implicit Arguments PartInt [a b Hab].
116 In one direction these operators are inverses.
119 inline "cic:/CoRN/ftc/PartInterval/int_part_int.con".
126 Section Equivalences.
129 (*#* **Mappings Preserve Operations
131 We now prove that all the operations we have defined on both sets are
132 preserved by [PartInt].
134 %\begin{convention}% Let [F,G] be partial functions and [a,b:IR] and
135 denote by [I] the interval [[a,b]]. Let [f,g] be setoid functions of
136 type [I->IR] equal respectively to [F] and [G] in [I].
140 inline "cic:/CoRN/ftc/PartInterval/F.var".
142 inline "cic:/CoRN/ftc/PartInterval/G.var".
144 inline "cic:/CoRN/ftc/PartInterval/a.var".
146 inline "cic:/CoRN/ftc/PartInterval/b.var".
148 inline "cic:/CoRN/ftc/PartInterval/c.var".
150 inline "cic:/CoRN/ftc/PartInterval/Hab.var".
154 inline "cic:/CoRN/ftc/PartInterval/I.con".
158 inline "cic:/CoRN/ftc/PartInterval/f.var".
160 inline "cic:/CoRN/ftc/PartInterval/g.var".
162 inline "cic:/CoRN/ftc/PartInterval/Ff.var".
164 inline "cic:/CoRN/ftc/PartInterval/Gg.var".
166 inline "cic:/CoRN/ftc/PartInterval/part_int_const.con".
168 inline "cic:/CoRN/ftc/PartInterval/part_int_id.con".
170 inline "cic:/CoRN/ftc/PartInterval/part_int_plus.con".
172 inline "cic:/CoRN/ftc/PartInterval/part_int_inv.con".
174 inline "cic:/CoRN/ftc/PartInterval/part_int_minus.con".
176 inline "cic:/CoRN/ftc/PartInterval/part_int_mult.con".
178 inline "cic:/CoRN/ftc/PartInterval/part_int_nth.con".
182 inline "cic:/CoRN/ftc/PartInterval/HG.var".
184 inline "cic:/CoRN/ftc/PartInterval/Hg.var".
188 inline "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
190 inline "cic:/CoRN/ftc/PartInterval/part_int_div.con".