contDiff — Mathlib

English

A continuous affine map between normed vector spaces is smooth; i.e., it is C^∞ in the sense of ContDiff for any level n.

Русский

Непрерывная аффинная карта между нормированными векторами пространствами гладна; то есть она бесконечно дифференцируема (ContDiff по любому n).

LaTeX

$$$\text{contDiff}_{\mathbb{K}}(n, f) \\quad \text{for all } n, f: V \to W \,\text{is smooth}$$$

Lean4

/-- A continuous affine map between normed vector spaces is smooth. -/
theorem contDiff {n : WithTop ℕ∞} (f : V →ᴬ[𝕜] W) : ContDiff 𝕜 n f :=
  by
  rw [f.decomp]
  apply f.contLinear.contDiff.add
  exact contDiff_const

Похожие утверждения