star_star — Mathlib

English

If f is differentiable at z, then star ∘ f ∘ star is differentiable at star z.

Русский

Если f дифференцируема в z, то star ∘ f ∘ star дифференцируема в star z.

LaTeX

$$$\\text{DifferentiableAt}_{\\mathbb{K}}(f,z) \\Rightarrow \\text{DifferentiableAt}_{\\mathbb{K}}(\\mathrm{star} \\circ f \\circ \\mathrm{star}, \\mathrm{star}(z))$$$

Lean4

/-- If `f` is differentiable at `z`, then `star ∘ f ∘ star` is differentiable at `star z`. -/
@[fun_prop]
theorem star_star {f : E → F} {z : E} (hf : DifferentiableAt 𝕜 f z) : DifferentiableAt 𝕜 (star ∘ f ∘ star) (star z) :=
  hf.hasFDerivAt.star_star.differentiableAt

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