hasDerivWithinAt_inter — Mathlib

English

If t ∈ 𝓝 x, then HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x.

Русский

Если t является обычной окрестностью x, то пересечение с t не меняет наличие производной внутри s.

LaTeX

$$$\text{HasDerivWithinAt } f\; f'\; (s \cap t)\; x \iff \text{HasDerivWithinAt } f\; f'\; s\; x \\text{ при } t \in \mathcal{nhds}(x)$$$

Lean4

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

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