clm_comp — Mathlib

English

Let c: E → L(G,H) and d: E → L(F,G) be differentiable on the entire space. Then the map y ↦ c(y) ∘ d(y) is differentiable on the whole space.

Русский

Пусть c: E → L(G,H) и d: E → L(F,G) дифференцируемы на всем пространстве. Тогда y ↦ c(y) ∘ d(y) дифференцируемо на всём пространстве.

LaTeX

$$$ \operatorname{Differentiable}_{\mathbb{K}} c \land \operatorname{Differentiable}_{\mathbb{K}} d \Rightarrow \operatorname{Differentiable}_{\mathbb{K}}\bigl( y \mapsto c(y) \circ d(y) \bigr)$$$

Lean4

@[fun_prop]
theorem clm_comp (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) : Differentiable 𝕜 fun y => (c y).comp (d y) :=
  fun x => (hc x).clm_comp (hd x)

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