star — Mathlib

English

If HasDerivWithinAt g g' s x then HasDerivWithinAt (star ∘ g) (star g') s x.

Русский

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

LaTeX

$$HasDerivWithinAt g g' s x → HasDerivWithinAt (fun x => star (g x)) (star g') s x$$

Lean4

protected nonrec theorem star (h : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => star (f x)) (star f') s x :=
  h.star

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