star — Mathlib

English

If HasDerivAtFilter f f' x L, then star ∘ f ∘ conj has derivative star f' at x.

Русский

Если у f есть производная в фильтре HasDerivAtFilter, то звёздочка композиции с conj сохраняет производную как conj f'.

LaTeX

$$HasDerivAtFilter f f' x L → HasDerivAtFilter (fun x => star (f x)) (star f') x L$$

Lean4

protected nonrec theorem star (h : HasDerivAtFilter f f' x L) : HasDerivAtFilter (fun x => star (f x)) (star f') x L :=
  by simpa using h.star.hasDerivAtFilter

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