mono — Mathlib

English

If HasDerivAtFilter f f' x holds for a filter L2 and L1 ≤ L2, then HasDerivAtFilter f f' x holds for L1 as well.

Русский

Если существует производная в точке x относительно фильтра L2, и L1 меньше или равно L2, то существование производной относительно L1 следует также.

LaTeX

$$$\text{HasDerivAtFilter } f\; f'\; x\; L_2 \Longrightarrow (L_1 \le L_2) \Rightarrow \text{HasDerivAtFilter } f\; f'\; x\; L_1$$$

Lean4

theorem mono (h : HasDerivAtFilter f f' x L₂) (hst : L₁ ≤ L₂) : HasDerivAtFilter f f' x L₁ :=
  HasFDerivAtFilter.mono h hst

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