matita/contribs/CoRN-Decl/ftc/MoreFunctions.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/MoreFunctions".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
  22
  23 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
  24
  25 include "ftc/MoreIntervals.ma".
  26
  27 (* UNEXPORTED
  28 Opaque Min Max.
  29 *)
  30
  31 (* UNEXPORTED
  32 Section Basic_Results
  33 *)
  34
  35 (*#* *More about Functions
  36
  37 Here we state all the main results about properties of functions that
  38 we already proved for compact intervals in the more general setting of
  39 arbitrary intervals.
  40
  41 %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions.
  42 %\end{convention}%
  43
  44 **Continuity
  45 *)
  46
  47 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var".
  48
  49 (*#*
  50 Trivial stuff.
  51 *)
  52
  53 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con".
  54
  55 (*#*
  56 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
  57 %\end{convention}%
  58 *)
  59
  60 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var".
  61
  62 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var".
  63
  64 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var".
  65
  66 inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con".
  67
  68 (* begin show *)
  69
  70 alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var".
  71
  72 (* end show *)
  73
  74 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con".
  75
  76 inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con".
  77
  78 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con".
  79
  80 (* UNEXPORTED
  81 End Basic_Results
  82 *)
  83
  84 (* UNEXPORTED
  85 Hint Resolve Continuous_imp_inc: included.
  86 *)
  87
  88 (* UNEXPORTED
  89 Section Other_Results
  90 *)
  91
  92 (*#*
  93 The usual stuff.
  94 *)
  95
  96 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var".
  97
  98 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var".
  99
 100 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var".
 101
 102 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con".
 103
 104 (* begin show *)
 105
 106 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var".
 107
 108 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var".
 109
 110 (* end show *)
 111
 112 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con".
 113
 114 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con".
 115
 116 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con".
 117
 118 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con".
 119
 120 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con".
 121
 122 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con".
 123
 124 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con".
 125
 126 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con".
 127
 128 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con".
 129
 130 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con".
 131
 132 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con".
 133
 134 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con".
 135
 136 (* UNEXPORTED
 137 End Other_Results
 138 *)
 139
 140 (* UNEXPORTED
 141 Hint Resolve continuous_compact Continuous_const Continuous_id
 142   Continuous_plus Continuous_inv Continuous_minus Continuous_mult
 143   Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
 144 *)
 145
 146 (* UNEXPORTED
 147 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
 148 *)
 149
 150 (* UNEXPORTED
 151 Section Corollaries
 152 *)
 153
 154 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var".
 155
 156 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var".
 157
 158 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var".
 159
 160 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var".
 161
 162 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var".
 163
 164 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var".
 165
 166 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con".
 167
 168 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con".
 169
 170 (* UNEXPORTED
 171 End Corollaries
 172 *)
 173
 174 (* UNEXPORTED
 175 Hint Resolve Continuous_div: continuous.
 176 *)
 177
 178 (* UNEXPORTED
 179 Section Sums
 180 *)
 181
 182 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var".
 183
 184 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
 185
 186 (*#*
 187 %\begin{convention}% Assume [f] is a sequence of continuous functions.
 188 %\end{convention}%
 189 *)
 190
 191 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var".
 192
 193 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var".
 194
 195 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con".
 196
 197 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con".
 198
 199 (* UNEXPORTED
 200 End Sums
 201 *)
 202
 203 (* UNEXPORTED
 204 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
 205 *)
 206
 207 (* UNEXPORTED
 208 Section Basic_Properties
 209 *)
 210
 211 (*#* **Derivative
 212
 213 Derivative is not that much different.
 214
 215 %\begin{convention}% From this point on we assume [I] to be proper.
 216 %\end{convention}%
 217 *)
 218
 219 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var".
 220
 221 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var".
 222
 223 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var".
 224
 225 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var".
 226
 227 alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var".
 228
 229 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con".
 230
 231 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con".
 232
 233 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con".
 234
 235 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con".
 236
 237 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con".
 238
 239 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con".
 240
 241 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con".
 242
 243 (* UNEXPORTED
 244 End Basic_Properties
 245 *)
 246
 247 (* UNEXPORTED
 248 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
 249 *)
 250
 251 (* UNEXPORTED
 252 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
 253   continuous.
 254 *)
 255
 256 (* UNEXPORTED
 257 Section More_Results
 258 *)
 259
 260 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var".
 261
 262 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var".
 263
 264 (*#*
 265 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
 266 %\end{convention}%
 267 *)
 268
 269 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var".
 270
 271 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var".
 272
 273 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var".
 274
 275 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var".
 276
 277 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var".
 278
 279 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var".
 280
 281 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con".
 282
 283 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con".
 284
 285 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con".
 286
 287 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con".
 288
 289 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con".
 290
 291 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con".
 292
 293 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con".
 294
 295 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con".
 296
 297 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con".
 298
 299 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con".
 300
 301 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con".
 302
 303 (* UNEXPORTED
 304 End More_Results
 305 *)
 306
 307 (* UNEXPORTED
 308 Section More_Corollaries
 309 *)
 310
 311 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var".
 312
 313 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var".
 314
 315 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var".
 316
 317 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var".
 318
 319 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var".
 320
 321 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var".
 322
 323 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var".
 324
 325 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var".
 326
 327 (* begin show *)
 328
 329 alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var".
 330
 331 (* end show *)
 332
 333 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con".
 334
 335 (* UNEXPORTED
 336 End More_Corollaries
 337 *)
 338
 339 (* UNEXPORTED
 340 Section More_Sums
 341 *)
 342
 343 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var".
 344
 345 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var".
 346
 347 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con".
 348
 349 (* begin show *)
 350
 351 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var".
 352
 353 alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var".
 354
 355 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var".
 356
 357 (* end show *)
 358
 359 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con".
 360
 361 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con".
 362
 363 (* UNEXPORTED
 364 End More_Sums
 365 *)
 366
 367 (* UNEXPORTED
 368 Section Diffble_Basic_Properties
 369 *)
 370
 371 (*#* **Differentiability
 372
 373 Mutatis mutandis for differentiability.
 374 *)
 375
 376 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var".
 377
 378 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var".
 379
 380 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con".
 381
 382 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con".
 383
 384 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con".
 385
 386 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var".
 387
 388 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var".
 389
 390 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var".
 391
 392 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var".
 393
 394 (*#*
 395 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
 396 %\end{convention}%
 397 *)
 398
 399 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con".
 400
 401 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con".
 402
 403 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con".
 404
 405 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con".
 406
 407 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con".
 408
 409 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con".
 410
 411 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con".
 412
 413 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con".
 414
 415 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con".
 416
 417 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con".
 418
 419 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con".
 420
 421 (* UNEXPORTED
 422 End Diffble_Basic_Properties
 423 *)
 424
 425 (* UNEXPORTED
 426 Hint Immediate Diffble_imp_inc: included.
 427 *)
 428
 429 (* UNEXPORTED
 430 Section Diffble_Corollaries
 431 *)
 432
 433 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var".
 434
 435 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var".
 436
 437 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var".
 438
 439 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var".
 440
 441 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var".
 442
 443 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var".
 444
 445 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con".
 446
 447 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con".
 448
 449 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con".
 450
 451 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con".
 452
 453 (* UNEXPORTED
 454 End Diffble_Corollaries
 455 *)
 456
 457 (* UNEXPORTED
 458 Section Nth_Derivative
 459 *)
 460
 461 (*#* **Nth Derivative
 462
 463 Higher order derivatives pose more interesting problems.  It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
 464 *)
 465
 466 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var".
 467
 468 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var".
 469
 470 (* UNEXPORTED
 471 Section Definitions
 472 *)
 473
 474 (*#*
 475 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
 476 %\end{convention}%
 477 *)
 478
 479 alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var".
 480
 481 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var".
 482
 483 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var".
 484
 485 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con".
 486
 487 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
 488  (* begin hide *).con".
 489
 490 (* end hide *)
 491
 492 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con".
 493
 494 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con".
 495
 496 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con".
 497
 498 (* UNEXPORTED
 499 End Definitions
 500 *)
 501
 502 (* UNEXPORTED
 503 Section Basic_Results
 504 *)
 505
 506 (*#*
 507 All the usual results hold.
 508 *)
 509
 510 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con".
 511
 512 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con".
 513
 514 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con".
 515
 516 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con".
 517
 518 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con".
 519
 520 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con".
 521
 522 inline "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con".
 523
 524 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con".
 525
 526 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con".
 527
 528 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con".
 529
 530 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con".
 531
 532 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con".
 533
 534 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con".
 535
 536 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con".
 537
 538 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con".
 539
 540 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con".
 541
 542 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con".
 543
 544 (* UNEXPORTED
 545 End Basic_Results
 546 *)
 547
 548 (* UNEXPORTED
 549 Section More_Results
 550 *)
 551
 552 (*#*
 553 Some new results hold, too:
 554 *)
 555
 556 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con".
 557
 558 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con".
 559
 560 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con".
 561
 562 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con".
 563
 564 (*#*
 565 Some useful characterization results.
 566 *)
 567
 568 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con".
 569
 570 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con".
 571
 572 (* UNEXPORTED
 573 End More_Results
 574 *)
 575
 576 (* UNEXPORTED
 577 Section Derivating_Diffble
 578 *)
 579
 580 (*#*
 581 As a special case we get a differentiation operator%\ldots%#...#
 582 *)
 583
 584 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var".
 585
 586 (* begin show *)
 587
 588 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var".
 589
 590 (* end show *)
 591
 592 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con".
 593
 594 inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con".
 595
 596 (* UNEXPORTED
 597 End Derivating_Diffble
 598 *)
 599
 600 (* UNEXPORTED
 601 Section Corollaries
 602 *)
 603
 604 (*#*
 605 %\ldots%#...# for which the expected property also holds.
 606 *)
 607
 608 inline "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con".
 609
 610 (*#*
 611 Some more interesting properties.
 612 *)
 613
 614 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con".
 615
 616 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con".
 617
 618 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con".
 619
 620 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con".
 621
 622 (* UNEXPORTED
 623 End Corollaries
 624 *)
 625
 626 (* UNEXPORTED
 627 End Nth_Derivative
 628 *)
 629
 630 (* UNEXPORTED
 631 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
 632   Derivative_minus Derivative_mult Derivative_scal Derivative_nth
 633   Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
 634   Derivative_Sum: derivate.
 635 *)
 636
 637 (* UNEXPORTED
 638 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
 639   included.
 640 *)
 641
 642 (* UNEXPORTED
 643 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
 644 *)
 645
 646 (* UNEXPORTED
 647 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':
 648   continuous.
 649 *)
 650