dist_iteratedFDerivWithin_zero — Mathlib

English

The zero-derivative equality holds again with a composition form.

Русский

Повторное утверждение равенства нулевой производной через композицию.

LaTeX

$$$$\text{iteratedFDerivWithin}(\mathbb{k},0,f,s) = (\text{continuousMultilinearCurryFin0 }\mathbb{k} E F)^{-1} \circ f.$$$$

Lean4

@[simp]
theorem dist_iteratedFDerivWithin_zero (f : E → F) (s : Set E) (x : E) (g : E → F) (t : Set E) (y : E) :
    dist (iteratedFDerivWithin 𝕜 0 f s x) (iteratedFDerivWithin 𝕜 0 g t y) = dist (f x) (g y) := by
  simp only [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.dist_map]

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