hasDerivAt_iff_tendsto_slope_left_right

English

For a linear order domain, HasDerivAt f f' x is equivalent to slope tending to f' from both sides.

Русский

Для линейного порядка производная существует тогда и только когда наклон слева и справа стремится к той же f'.

LaTeX

$$$HasDerivAt f f' x \\iff (Tendsto (slope f x) (\\mathcal{N}_{x}^{<}) (\\mathcal{N} f') \\wedge Tendsto (slope f x) (\\mathcal{N}_{x}^{>}) (\\mathcal{N} f'))$$$

Lean4

theorem hasDerivAt_iff_tendsto_slope_left_right [LinearOrder 𝕜] :
    HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[<] x) (𝓝 f') ∧ Tendsto (slope f x) (𝓝[>] x) (𝓝 f') := by
  simp [hasDerivAt_iff_tendsto_slope, ← Iio_union_Ioi, nhdsWithin_union]

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