mono — Mathlib

English

If a map is line-differentiable within a larger set t, then it is line-differentiable within any smaller subset s with s ⊆ t.

Русский

Если функция дифференцируема вдоль линии внутри большего множества t, то она линейно дифференцируема и внутри любого меньшего подмножества s, где s ⊆ t.

LaTeX

$$$\text{LineDifferentiableWithinAt}_{\mathbb{k}}(f, t, x, v) \Rightarrow \text{LineDifferentiableWithinAt}_{\mathbb{k}}(f, s, x, v) \text{ whenever } s \subseteq t$$$

Lean4

theorem mono (h : LineDifferentiableWithinAt 𝕜 f t x v) (st : s ⊆ t) : LineDifferentiableWithinAt 𝕜 f s x v :=
  (h.hasLineDerivWithinAt.mono st).lineDifferentiableWithinAt

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