hasFDerivWithinAt_fst — Mathlib

English

Within s, fderiv of product map equals product of fderivWithin: fderivWithin 𝕜 (λ x, (f1 x, f2 x)) s x = (fderivWithin 𝕜 f1 s x).prod (fderivWithin 𝕜 f2 s x).

Русский

Внутри s производная от произведения равна произведению производных внутри: fderivWithin 𝕜 (λ x, (f1 x, f2 x)) s x = ...

LaTeX

$$$\text{fderivWithin } 𝕜 (\lambda x:E, (f_1 x,f_2 x)) s x = (\text{fderivWithin } 𝕜 f_1 s x).prod (\text{fderivWithin } 𝕜 f_2 s x)$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt_fst {s : Set (E × F)} : HasFDerivWithinAt (@Prod.fst E F) (fst 𝕜 E F) s p :=
  hasFDerivAtFilter_fst

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