English
If a line derivative exists on a set s, then it also exists on any subset t ⊆ s; the derivative value is preserved accordingly when restricted to t.
Русский
Если существует прямая производная на множестве s, то она существует и на любом подмножестве t ⊆ s; значение производной сохраняется при ограничении до t.
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
/-- `f` has the derivative `f'` at the point `x` along the direction `v` in the set `s`.
That is, `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0` and `x + t v ∈ s`.
Note that this definition is less well behaved than the total Fréchet derivative, which
should generally be favored over this one. -/
def HasLineDerivWithinAt (f : E → F) (f' : F) (s : Set E) (x : E) (v : E) :=
HasDerivWithinAt (fun t ↦ f (x + t • v)) f' ((fun t ↦ x + t • v) ⁻¹' s) (0 : 𝕜)
