prodMk — Mathlib

English

If f1 and f2 are differentiable on a set s, then the map x ↦ (f1 x, f2 x) is differentiable on s.

Русский

Если f1 и f2 дифференцируемы на множестве s, то отображение x ↦ (f1 x, f2 x) дифференцируемо на s.

LaTeX

$$$\text{DifferentiableOn } 𝕜 f_1\ s \to \text{ DifferentiableOn } 𝕜 f_2\ s \to \text{DifferentiableOn } 𝕜 (\lambda x:E, (f_1 x,f_2 x)) s$$$

Lean4

@[fun_prop]
theorem prodMk (hf₁ : DifferentiableOn 𝕜 f₁ s) (hf₂ : DifferentiableOn 𝕜 f₂ s) :
    DifferentiableOn 𝕜 (fun x : E => (f₁ x, f₂ x)) s := fun x hx => (hf₁ x hx).prodMk (hf₂ x hx)

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