comp_hasFDerivWithinAt_iff — Mathlib

English

A variant of HasFDerivWithinAt for precomposed maps with symmetries, expressing the same derivative relation via symmetries.

Русский

Вариант HasFDerivWithinAt для предваренного отображения с симметриями, выражающий ту же зависимость производной через симметрии.

LaTeX

$$$HasFDerivWithinAt (iso ∘ f) f' s x \iff HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x$$$

Lean4

theorem comp_hasFDerivWithinAt_iff {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x :=
  by
  refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩
  simpa [Function.comp_def, ← ContinuousLinearMap.comp_assoc] using iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H

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