IndisputableMonolith.Foundation.GeneralizedDAlembert.SmoothnessTop

   1import Mathlib
   2
   3/-!
   4  Finite-to-top smoothness helper for the continuous-combiner d'Alembert
   5  route.
   6
   7  Mathlib records `C^\infty` smoothness as `ContDiff 𝕜 ⊤ f`. The theorem
   8  `contDiff_infty` identifies this with `C^n` smoothness for every finite
   9  `n`. This file isolates that API step so the main generalized d'Alembert
  10  module does not carry it as an axiom.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Foundation
  15namespace GeneralizedDAlembert
  16namespace SmoothnessTop
  17
  18theorem contDiff_top_of_contDiff_nat
  19    {f : ℝ → ℝ}
  20    (hFinite : ∀ n : ℕ, ContDiff ℝ n f) :
  21    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) f := by
  22  exact (contDiff_infty).2 hFinite
  23
  24end SmoothnessTop
  25end GeneralizedDAlembert
  26end Foundation
  27end IndisputableMonolith
  28