prodMk — Mathlib

English

Let f1: 𝕜 → F and f2: 𝕜 → G be differentiable along a filter L at x with derivatives f1' and f2'. Then the map x ↦ (f1(x), f2(x)) has derivative (f1', f2') at x along L.

Русский

Пусть f1: 𝕜 → F и f2: 𝕜 → G дифференцируемы вдоль фильтра L в точке x с производными f1' и f2'. Тогда отображение x ↦ (f1(x), f2(x)) имеет производную (f1', f2') в точке x вдоль L.

LaTeX

$$$HasDerivAtFilter f_1 f_1' x L \to HasDerivAtFilter f_2 f_2' x L \to HasDerivAtFilter (\lambda t, (f_1 t, f_2 t)) (f_1', f_2') x L$$$

Lean4

nonrec theorem prodMk (hf₁ : HasDerivAtFilter f₁ f₁' x L) (hf₂ : HasDerivAtFilter f₂ f₂' x L) :
    HasDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁', f₂') x L :=
  hf₁.prodMk hf₂

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