fderivWithin_def — Mathlib

English

A derivative at a filter L is equivalent to a little-o condition on the difference quotient: HasFDerivAtFilter f f' x L is equivalent to the expression (f x' - f x - f'(x' - x)) =o[L] (x' - x).

Русский

Производная в фильтре эквивалентна условию малого o для разности: f(x') − f(x) − f'(x' − x) =o[L](x' − x).

LaTeX

$$$\text{HasFDerivAtFilter } f f' x L \iff (f x' - f x - f'(x' - x)) =o[L] (x' - x)$$$

Lean4

theorem fderivWithin_def : eta_helper Eq✝ @fderivWithin.{} @(delta% @definition✝) :=
  by
  intros
  delta fderivWithin
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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