eq — Mathlib · SciLib

English

If f is not MDifferentiableWithinAt, then mfderivWithin is zero.

Русский

Если f не дифференцируемо внутри, то mfderivWithin равно нулю.

LaTeX

$$$\text{mfderivWithin } I I' f s x = 0 \;\text{ if } ¬ MDifferentiableWithinAt I I' f s x$$$

Lean4

/-- `UniqueMDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative. -/
protected nonrec theorem eq (U : UniqueMDiffWithinAt I s x) (h : HasMFDerivWithinAt I I' f s x f')
    (h₁ : HasMFDerivWithinAt I I' f s x f₁') : f' = f₁' := by
  -- `by apply` because the instances can be found in the term but not in the goal.
  apply U.eq h.2 h₁.2

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