mono — Mathlib

English

If a derivative exists along a filter L₂, then it also exists along any coarser filter L₁ with L₁ ≤ L₂, i.e., HasFDerivAtFilter f f' x L₁ follows from HasFDerivAtFilter f f' x L₂ when L₁ ≤ L₂.

Русский

Если производная существует вдоль фильтра L₂, то она существует и вдоль любого более грубого фильтра L₁ при L₁ ≤ L₂.

LaTeX

$$$$\\text{HasFDerivAtFilter } f\\,f'\\,x\\,L_1 \\text{ follows from }\\ \\text{HasFDerivAtFilter } f\\,f'\\,x\\,L_2 \\text{ when } L_1 \\le L_2.$$$$

Lean4

nonrec theorem mono (h : HasFDerivAtFilter f f' x L₂) (hst : L₁ ≤ L₂) : HasFDerivAtFilter f f' x L₁ :=
  .of_isLittleOTVS <| h.isLittleOTVS.mono hst

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