hasDerivWithinAt_inter' — Mathlib

English

If t is a neighborhood of x within s, then HasDerivWithinAt f f' (s ∩ t) x is equivalent to HasDerivWithinAt f f' s x.

Русский

Если t является окрестностью x внутри s, то производная внутри (s ∩ t) эквивалентна внутри s.

LaTeX

$$$\text{HasDerivWithinAt } f\; f'\; (s \cap t)\; x \iff \text{HasDerivWithinAt } f\; f'\; s\; x\; (t \in nhdsWithin(x,s))$$$

Lean4

theorem hasDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) : HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x :=
  hasFDerivWithinAt_inter' h

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