hasMFDerivAt_unique — Mathlib

English

Equivalence of HasMFDerivWithinAt on univ and HasMFDerivAt.

Русский

Эквивалентность HasMFDerivWithinAt на univ и HasMFDerivAt.

LaTeX

$$hasMFDerivWithinAt_univ : HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f'$$

Lean4

theorem hasMFDerivAt_unique (h₀ : HasMFDerivAt I I' f x f₀') (h₁ : HasMFDerivAt I I' f x f₁') : f₀' = f₁' :=
  by
  rw [← hasMFDerivWithinAt_univ] at h₀ h₁
  exact (uniqueMDiffWithinAt_univ I).eq h₀ h₁

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