helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval".
  18
  19 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 IntervalFunct
  23 *)
  24
  25 (* UNEXPORTED
  26 Section Conversion.
  27 *)
  28
  29 (*#* *Correspondence
  30
  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.
  36
  37 **Mappings
  38
  39 We begin by defining the map from partial functions to setoid
  40 functions as simply being the restriction of the partial function to
  41 the interval [[a,b]].
  42
  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].
  45 %\end{convention}%
  46 *)
  47
  48 inline cic:/CoRN/ftc/PartInterval/F.var.
  49
  50 inline cic:/CoRN/ftc/PartInterval/a.var.
  51
  52 inline cic:/CoRN/ftc/PartInterval/b.var.
  53
  54 inline cic:/CoRN/ftc/PartInterval/Hab.var.
  55
  56 (* begin hide *)
  57
  58 inline cic:/CoRN/ftc/PartInterval/I.con.
  59
  60 (* end hide *)
  61
  62 inline cic:/CoRN/ftc/PartInterval/Hf.var.
  63
  64 inline cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con.
  65
  66 inline cic:/CoRN/ftc/PartInterval/IntPartIR.con.
  67
  68 (* UNEXPORTED
  69 End Conversion.
  70 *)
  71
  72 (* UNEXPORTED
  73 Implicit Arguments IntPartIR [F a b Hab].
  74 *)
  75
  76 (* UNEXPORTED
  77 Section AntiConversion.
  78 *)
  79
  80 (*#*
  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.
  83 *)
  84
  85 inline cic:/CoRN/ftc/PartInterval/a.var.
  86
  87 inline cic:/CoRN/ftc/PartInterval/b.var.
  88
  89 inline cic:/CoRN/ftc/PartInterval/Hab.var.
  90
  91 (* begin hide *)
  92
  93 inline cic:/CoRN/ftc/PartInterval/I.con.
  94
  95 (* end hide *)
  96
  97 inline cic:/CoRN/ftc/PartInterval/f.var.
  98
  99 inline cic:/CoRN/ftc/PartInterval/PartInt_strext.con.
 100
 101 inline cic:/CoRN/ftc/PartInterval/PartInt.con.
 102
 103 (* UNEXPORTED
 104 End AntiConversion.
 105 *)
 106
 107 (* UNEXPORTED
 108 Implicit Arguments PartInt [a b Hab].
 109 *)
 110
 111 (* UNEXPORTED
 112 Section Inverses.
 113 *)
 114
 115 (*#*
 116 In one direction these operators are inverses.
 117 *)
 118
 119 inline cic:/CoRN/ftc/PartInterval/int_part_int.con.
 120
 121 (* UNEXPORTED
 122 End Inverses.
 123 *)
 124
 125 (* UNEXPORTED
 126 Section Equivalences.
 127 *)
 128
 129 (*#* **Mappings Preserve Operations
 130
 131 We now prove that all the operations we have defined on both sets are
 132 preserved by [PartInt].
 133
 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].
 137 %\end{convention}%
 138 *)
 139
 140 inline cic:/CoRN/ftc/PartInterval/F.var.
 141
 142 inline cic:/CoRN/ftc/PartInterval/G.var.
 143
 144 inline cic:/CoRN/ftc/PartInterval/a.var.
 145
 146 inline cic:/CoRN/ftc/PartInterval/b.var.
 147
 148 inline cic:/CoRN/ftc/PartInterval/c.var.
 149
 150 inline cic:/CoRN/ftc/PartInterval/Hab.var.
 151
 152 (* begin hide *)
 153
 154 inline cic:/CoRN/ftc/PartInterval/I.con.
 155
 156 (* end hide *)
 157
 158 inline cic:/CoRN/ftc/PartInterval/f.var.
 159
 160 inline cic:/CoRN/ftc/PartInterval/g.var.
 161
 162 inline cic:/CoRN/ftc/PartInterval/Ff.var.
 163
 164 inline cic:/CoRN/ftc/PartInterval/Gg.var.
 165
 166 inline cic:/CoRN/ftc/PartInterval/part_int_const.con.
 167
 168 inline cic:/CoRN/ftc/PartInterval/part_int_id.con.
 169
 170 inline cic:/CoRN/ftc/PartInterval/part_int_plus.con.
 171
 172 inline cic:/CoRN/ftc/PartInterval/part_int_inv.con.
 173
 174 inline cic:/CoRN/ftc/PartInterval/part_int_minus.con.
 175
 176 inline cic:/CoRN/ftc/PartInterval/part_int_mult.con.
 177
 178 inline cic:/CoRN/ftc/PartInterval/part_int_nth.con.
 179
 180 (* begin show *)
 181
 182 inline cic:/CoRN/ftc/PartInterval/HG.var.
 183
 184 inline cic:/CoRN/ftc/PartInterval/Hg.var.
 185
 186 (* end show *)
 187
 188 inline cic:/CoRN/ftc/PartInterval/part_int_recip.con.
 189
 190 inline cic:/CoRN/ftc/PartInterval/part_int_div.con.
 191
 192 (* UNEXPORTED
 193 End Equivalences.
 194 *)
 195