hasFDerivWithinAt — Mathlib

English

If HasFDerivAtFilter f f' x L₂ holds and L₁ ≤ L₂, then HasFDerivAtFilter f f' x L₁ holds. The derivative property along finer filters persists under weakening the filter order.

Русский

Если HasFDerivAtFilter f f' x L₂ выполняется и L₁ ≤ L₂, то HasFDerivAtFilter f f' x L₁ выполняется.

LaTeX

$$$$\\text{HasFDerivAtFilter } f\\,f'\\,x\\,L_2 \\land L_1 \\le L_2 \\implies \\text{HasFDerivAtFilter } f\\,f'\\,x\\,L_1.$$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt (h : HasFDerivAt f f' x) : HasFDerivWithinAt f f' s x :=
  h.hasFDerivAtFilter inf_le_left

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