star — Mathlib

English

If HasStrictDerivAt f f' x, then HasStrictDerivAt (star ∘ f) (star f') x.

Русский

Если есть строгая производная, то звёздка сохраняет её: star(f) имеет производную star(f') в точке x.

LaTeX

$$HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => star (f x)) (star f') x$$

Lean4

protected nonrec theorem star (h : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => star (f x)) (star f') x := by
  simpa using h.star.hasStrictDerivAt

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