English
A fundamental equivalence: a family of continuous linear maps is C^n on s iff each fixed second argument is C^n on s.
Русский
Фундаментальная эквивалентность: семейство непрерывных линейных отображений является C^n на s тогда и только тогда, когда каждый фиксированный второй аргумент имеет C^n на s.
LaTeX
$$contDiffOn_clm_apply {f} {s} : ContDiffOn 𝕜 n f s ↔ ∀ y, ContDiffOn 𝕜 n (fun x => f x y) s$$
Lean4
/-- A family of continuous linear maps is `C^n` on `s` if all its applications are. -/
theorem contDiffOn_clm_apply {f : D → E →L[𝕜] F} {s : Set D} [FiniteDimensional 𝕜 E] :
ContDiffOn 𝕜 n f s ↔ ∀ y, ContDiffOn 𝕜 n (fun x => f x y) s :=
by
refine ⟨fun h y => h.clm_apply contDiffOn_const, fun h => ?_⟩
let d := finrank 𝕜 E
have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
let e₁ := ContinuousLinearEquiv.ofFinrankEq hd
let e₂ := (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))
rw [← id_comp f, ← e₂.symm_comp_self]
exact e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)
