ContinuousAffineMap.contDiff

theorem ContinuousAffineMap.contDiff : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W] {n : ℕ∞} (f : V →A[𝕜] W), ContDiff 𝕜 n ⇑f

The theorem states that for any continuous affine map 'f' from a normed vector space 'V' to another normed vector space 'W' over a nontrivially normed field '𝕜', 'f' is a smooth map. 'Smooth' here means that the map is continuously differentiable for any natural number 'n' or infinity (∞). In other words, an affine map that is continuous in a normed vector space setting is also smooth.

More concisely: Any continuous affine map between normed vector spaces over a nontrivially normed field is smooth (infinitely differentiable).