differentiableWithinAt_inter — Mathlib

English

If t is a neighborhood of x, then differentiability within s ∩ t at x is equivalent to differentiability within s at x.

Русский

Если t образует окрестность x, то дифференцируемость внутри s ∩ t в x эквивалентна дифференцируемости внутри s в x.

LaTeX

$$$\text{ht: } t \in 𝓝 x \Rightarrow \mathrm{DifferentiableWithinAt } 𝕜 f (s \cap t) x \iff \mathrm{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem differentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
    DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by
  simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]

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