hasFDerivWithinAt_inter — Mathlib

English

If HasFDerivWithinAt f f' s x and HasFDerivWithinAt f f' t x hold, then HasFDerivWithinAt f f' (s ∪ t) x holds.

Русский

Если существуют производные внутри s и внутри t в x, то существует внутри s ∪ t в x.

LaTeX

$$$ HasFDerivWithinAt f f' s x \\rightarrow HasFDerivWithinAt f f' t x \\rightarrow HasFDerivWithinAt f f' (s \\cup t) x. $$$

Lean4

theorem hasFDerivWithinAt_inter (h : t ∈ 𝓝 x) : HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x := by
  simp [HasFDerivWithinAt, nhdsWithin_restrict' s h]

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