differentiableWithinAt_inter' — Mathlib

English

If t is in the nhdsWithin of s at x, differentiability within s ∩ t at x is equivalent to differentiability within s at x.

Русский

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

LaTeX

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

Lean4

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

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