English
Characterization of contDiff for a CLM-valued map: contDiff for f is equivalent to contDiff of all coordinate maps x ↦ f x y.
Русский
Характеризация contDiff для отображения с непрерывной линейной картой: contDiff f эквивалентно contDiff всех координатных отображений x ↦ f x y.
LaTeX
$$contDiff_clm_apply {f} {s} : ContDiff 𝕜 n f ↔ ∀ y, ContDiff 𝕜 n fun x => ContinuousLinearMap.funLike.coe (f x) y$$
Lean4
theorem contDiff_clm_apply_iff {f : D → E →L[𝕜] F} [FiniteDimensional 𝕜 E] :
ContDiff 𝕜 n f ↔ ∀ y, ContDiff 𝕜 n fun x => f x y := by simp_rw [← contDiffOn_univ, contDiffOn_clm_apply]