hasStrictFDerivAt_euclidean — Mathlib

English

HasStrictFDerivAt f f' y in Euclidean space iff each coordinate map has the corresponding strict derivative.

Русский

У функции f, имеющей строгий производный в точке y, каждый координатный компонент имеет соответствующий строгий производный.

LaTeX

$$$\text{HasStrictFDerivAt}(f,f',y) \iff \forall i, \text{HasStrictFDerivAt}(f_i, (\Pi_i f')| ) y,$$$

Lean4

theorem hasStrictFDerivAt_euclidean :
    HasStrictFDerivAt f f' y ↔ ∀ i, HasStrictFDerivAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') y :=
  hasStrictFDerivAt_piLp _

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