contDiff_clm_apply_iff — Mathlib

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]

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