hasStrictFDerivAt_apply — Mathlib

English

For each index i, the map sending a family of objects to its i-th element has derivative equal to the i-th projection. In particular, the derivative of the evaluation map is the projection homomorphism.

Русский

Для каждого индекса i отображение совокупности объектов к i-й координате имеет производную, равную проекции на i-ю координату; следовательно, дифференцирование по координате совпадает с проекцией.

LaTeX

$$$\\text{HasStrictFDerivAt} \\big( f \\mapsto f(i) \\big) = \\text{ContinuousLinearMap.proj}_i.$$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_apply (i : ι) (f : ∀ i, F' i) :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) f :=
  by
  let id' := ContinuousLinearMap.id 𝕜 (∀ i, F' i)
  have h := ((hasStrictFDerivAt_pi' (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ' := id') (x := f))).1
  have h' : comp (proj i) id' = proj i := by ext; simp [id']
  rw [← h']; apply h; apply hasStrictFDerivAt_id

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