smul_const — Mathlib

English

If hc : DifferentiableWithinAt 𝕜 c s x, then for any f ∈ F, DifferentiableWithinAt 𝕜 (λ y. c(y) · f) s x.

Русский

Если hc : DifferentiableWithinAt 𝕜 c s x, то для любого f ∈ F, DifferentiableWithinAt 𝕜 (λ y. c(y) · f) s x.

LaTeX

$$$\ DifferentiableWithinAt\ 𝕜\ c\ s\ x \Rightarrow \forall f\in F, \ DifferentiableWithinAt\ 𝕜\ (\\lambda y. c(y) \\cdot f)\ s\ x$$$

Lean4

@[fun_prop]
theorem smul_const (hc : Differentiable 𝕜 c) (f : F) : Differentiable 𝕜 fun y => c y • f := fun x => (hc x).smul_const f

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