mfderivWithin_inter — Mathlib

English

If nhdsWithin x s = nhdsWithin x t, then MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x.

Русский

Если nhdsWithin x s = nhdsWithin x t, то MDifferentiableWithinAt I I' f s x эквивалентно MDifferentiableWithinAt I I' f t x.

LaTeX

$$$ 𝓝[s] x = 𝓝[t] x \Rightarrow (MDifferentiableWithinAt I I' f s x \iff MDifferentiableWithinAt I I' f t x) $$$

Lean4

theorem mfderivWithin_inter (ht : t ∈ 𝓝 x) : mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x := by
  rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]

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