hasLineDerivWithinAt — Mathlib

English

If a line-differentiable-within object exists, then its derivative within s is a valid HasLineDerivWithinAt object on s.

Русский

Если существует линейная производная внутри множества s, то её можно считать HasLineDerivWithinAt на s.

LaTeX

$$$hf: LineDifferentiableWithinAt 𝕜 f s x v \Rightarrow HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) s x v.$$$

Lean4

theorem hasLineDerivWithinAt (h : LineDifferentiableWithinAt 𝕜 f s x v) :
    HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) s x v :=
  DifferentiableWithinAt.hasDerivWithinAt h

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