fderivCLM_apply — Mathlib

English

The Fréchet derivative on Schwartz space is a continuous linear map from Schwartz(E, F) to Schwartz(E, E →L F). It sends each f to its derivative-valued map.

Русский

Фредхель производная на пространстве Шварца задаёт непрерывно линейное отображение от Schwartz(E,F) к Schwartz(E, E →L F); каждому f соответствует его производная как элемент Schwartz(E, E →L F).

LaTeX

$$$fderivCLM : \mathcal{S}(E, F) \to_L \mathcal{S}(E, (E \to_L F))$$$

Lean4

@[simp]
theorem fderivCLM_apply (f : 𝓢(E, F)) (x : E) : fderivCLM 𝕜 f x = fderiv ℝ f x :=
  rfl

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