hasFDerivWithinAt_inter' — Mathlib

English

For h: t ∈ 𝓝 x, HasFDerivWithinAt f f' (s ∩ t) x is equivalent to HasFDerivWithinAt f f' s x.

Русский

Если t ∈ 𝓝 x, то HasFDerivWithinAt f f' (s ∩ t) x эквивалентно HasFDerivWithinAt f f' s x.

LaTeX

$$$ (h : t \\in 𝓝 x) : HasFDerivWithinAt f f' (s \\cap t) x \\iff HasFDerivWithinAt f f' s x. $$$

Lean4

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

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