English
If h is HasLineDerivWithinAt 𝕜 f f' s x v, then for any scalar c, h.smul c gives HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v).
Русский
Пусть h есть HasLineDerivWithinAt 𝕜 f f' s x v, тогда для любого скаляра c выполняется h.smul c: HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v).
LaTeX
$$$$ HasLineDerivWithinAt 𝕜 f f' s x v \Rightarrow HasLineDerivWithinAt 𝕜 f (c \cdot f') s x (c \cdot v) $$$$
Lean4
theorem smul (h : HasLineDerivWithinAt 𝕜 f f' s x v) (c : 𝕜) : HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) :=
by
simp only [HasLineDerivWithinAt] at h ⊢
let g := fun (t : 𝕜) ↦ c • t
let s' := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
have A : HasDerivAt g c 0 := by simpa using (hasDerivAt_id (0 : 𝕜)).const_smul c
have B : HasDerivWithinAt (fun t ↦ f (x + t • v)) f' s' (g 0) := by simpa [g] using h
have Z := B.scomp (0 : 𝕜) A.hasDerivWithinAt (mapsTo_preimage g s')
simp only [g, s', Function.comp_def, smul_eq_mul, mul_comm c, ← smul_smul] at Z
convert Z
ext t
simp [← smul_smul]
