hasDerivWithinAt_Ioi_iff_Ici — Mathlib

English

For a partial order 𝕜, HasDerivWithinAt f f' (Ioi x) x holds iff HasDerivWithinAt f f' (Ici x) x.

Русский

Для частичного порядка 𝕜: HasDerivWithinAt на Ioi x эквивалентно HasDerivWithinAt на Ici x.

LaTeX

$$$\\mathrm{HasDerivWithinAt}(f,f',Ioi(x),x) \\iff \\mathrm{HasDerivWithinAt}(f,f',Ici(x),x).$$$

Lean4

@[simp]
theorem hasDerivWithinAt_Ioi_iff_Ici [PartialOrder 𝕜] :
    HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x := by
  rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]

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