helm/software/matita/contribs/procedural/CoRN/ftc/MoreFunctions.mma

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