`contDiff_top_of_contDiff_nat`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.GeneralizedDAlembert.SmoothnessTop
domain: Foundation
line: 18 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.GeneralizedDAlembert.SmoothnessTop on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

continuous_combiner_finite_smoothness_to_top IndisputableMonolith.Foundation.GeneralizedDAlembert

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.