mono — Mathlib

English

The HasLineDerivWithinAt concept describes the line derivative restricted to a subset s; if it exists on s, then it exists on any subset t ⊆ s with the same value.

Русский

HasLineDerivWithinAt описывает линейную производную по направлению на ограничении; она существует на s и сохраняется на любом t ⊆ s с тем же значением.

LaTeX

$$$$\forall 𝕜 f f' s t x v,\ HasLineDerivWithinAt 𝕜 f f' s x v \land t \subseteq s \Rightarrow HasLineDerivWithinAt 𝕜 f f' t x v.$$$$

Lean4

theorem mono (hf : HasLineDerivWithinAt 𝕜 f f' s x v) (hst : t ⊆ s) : HasLineDerivWithinAt 𝕜 f f' t x v :=
  HasDerivWithinAt.mono hf (preimage_mono hst)

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