hasFDerivWithinAt_comp_smul_iff_smul

English

For any nonzero c, HasFDerivWithinAt (f (c • ·)) is equivalent to HasFDerivWithinAt (c • f) with scaled domain and input.

Русский

Для любого ненулевого c имеет место эквивалентность HasFDerivWithinAt (f (c • ·)) и HasFDerivWithinAt (c • f) при масштабировании области и аргумента.

LaTeX

$$$$ HasFDerivWithinAt (f \\circ (c \\cdot \\cdot)) f' s x \\iff HasFDerivWithinAt (c \\cdot f) f' (c \\cdot s) (c \\cdot x) $$$$

Lean4

theorem hasFDerivWithinAt_comp_smul_iff_smul {c : 𝕜} (hc : c ≠ 0) :
    HasFDerivWithinAt (f <| c • ·) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x) :=
  by
  simp only [← hasFDerivWithinAt_comp_smul_smul_iff, Pi.smul_apply]
  lift c to 𝕜ˣ using IsUnit.mk0 c hc
  exact (ContinuousLinearEquiv.smulLeft c).comp_hasFDerivWithinAt_iff.symm

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