mono — Mathlib

English

If HasFDerivWithinAt f f' t x holds and s ⊆ t, then HasFDerivWithinAt f f' s x holds. Narrowing the domain does not destroy the derivative existence.

Русский

Если HasFDerivWithinAt f f' t x и s ⊆ t, то HasFDerivWithinAt f f' s x.

LaTeX

$$$$\\text{HasFDerivWithinAt } f\\,f'\\,t\\,x \\; \\wedge\\; s \\subseteq t \\;\; \\Rightarrow \\; \\text{HasFDerivWithinAt } f\\,f'\\,s\\,x.$$$$

Lean4

nonrec theorem mono (h : HasFDerivWithinAt f f' t x) (hst : s ⊆ t) : HasFDerivWithinAt f f' s x :=
  h.mono <| nhdsWithin_mono _ hst

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