fderivWithin_inter — Mathlib

English

If s ⊆ t, UniqueDiffWithinAt 𝕜 s x, and f is differentiable within t at x, then fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x.

Русский

Если s ⊆ t, x уникально дифференцируем внутри s и f дифференцируема внутри t в x, то fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x.

LaTeX

$$∥(st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x)∥ : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x$$

Lean4

theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by
  classical simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

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