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".
19 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
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.