Smoothness through a closed linear isometric inclusion

For finite orders and ∞, smoothness can be checked after composing with a linear isometry whose range is closed. Derivatives remain in the closed range and hence lift, with their norms and continuity preserved. This gives the smooth alternating-map pullback needed for differential-form coordinate changes without a characteristic restriction. The analytic order ω is not covered by this criterion.

theorem LinearIsometry.comp_contDiff_iff {𝕜 : Type u_1} {D : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (i : E →ₗᵢ[𝕜] F) (hi : IsClosed (Set.range ⇑i)) {f : D → E} {n : ℕ∞} : ContDiff 𝕜 (↑n) (⇑i ∘ f) ↔ ContDiff 𝕜 (↑n) f

For finite orders and ∞, a closed linear isometric inclusion reflects smoothness. No completeness assumption is needed.