differentiable_star_iff — Mathlib

English

Differentiable 𝕜 (fun y => star (f y)) is equivalent to Differentiable 𝕜 f.

Русский

Дифференцируемость функции f эквивалентна дифференцируемости функции y ↦ star(f(y)).

LaTeX

$$$\\text{Differentiable}_{\\mathbb{K}}(\\lambda y. \\mathrm{star}(f(y))) \\iff \\text{Differentiable}_{\\mathbb{K}}(f)$$$

Lean4

@[simp]
theorem differentiable_star_iff : (Differentiable 𝕜 fun y => star (f y)) ↔ Differentiable 𝕜 f :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_differentiable_iff

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