English
Let f: E → F, and let x ∈ E and v ∈ E. Then f is line-differentiable along v at x, when considered on the whole ambient space, if and only if f is line-differentiable along v at x when viewed without restricting the domain (i.e., the line through x in the direction v).
Русский
Пусть f: E → F, пусть x ∈ E и v ∈ E. Тогда линейно дифференцируемость вдоль направления v в точке x на всём пространстве эквивалентна линейной дифференцируемости вдоль v в точке x без ограничения области (по всей линейке через x).
LaTeX
$$$\\mathrm{LineDifferentiableWithinAt}_{\\mathbb{k}}(f, \\mathrm{univ}, x, v) \\;\\Longleftrightarrow\\; \\mathrm{LineDifferentiableAt}_{\\mathbb{k}}(f, x, v)$$$
Lean4
theorem lineDifferentiableWithinAt_univ : LineDifferentiableWithinAt 𝕜 f univ x v ↔ LineDifferentiableAt 𝕜 f x v := by
simp only [LineDifferentiableWithinAt, LineDifferentiableAt, preimage_univ, differentiableWithinAt_univ]
