restrictScalars — Mathlib

English

If HasFDerivAtFilter f f' x L holds, then f has the restricted derivative f'.restrictScalars 𝕜 at x with the same filter L.

Русский

Если выполняется HasFDerivAtFilter f f' x L, то у f есть ограниченная производная после снятия скаляра: f'.restrictScalars 𝕜 при x с тем же фильтром L.

LaTeX

$$$ HasFDerivAtFilter\ f\ f'\ x\ L \Rightarrow\ HasFDerivAtFilter\ f\ (f'.restrictScalars\ 𝕜)\ x\ L $$$

Lean4

theorem restrictScalars {L} (h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter f (f'.restrictScalars 𝕜) x L :=
  .of_isLittleO h.isLittleO

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