mono — Mathlib

English

If HasDerivWithinAt f f' t x holds and s ⊆ t, then HasDerivWithinAt f f' s x holds.

Русский

Если существует производная внутри t, и s ⊆ t, то существует производная внутри s.

LaTeX

$$$\text{HasDerivWithinAt } f\; f'\; t\; x \to (s \subseteq t) \Rightarrow \text{HasDerivWithinAt } f\; f'\; s\; x$$$

Lean4

theorem mono (h : HasDerivWithinAt f f' t x) (hst : s ⊆ t) : HasDerivWithinAt f f' s x :=
  HasFDerivWithinAt.mono h hst

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