hasFDerivAt_of_subsingleton — Mathlib

English

If E is a subsingleton, HasFDerivAt f 0 x holds for any f and x.

Русский

Если множество E состоит из одного элемента, то HasFDerivAt f 0 x верно для любой f и x.

LaTeX

$$$HasFDerivAt f 0 x$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_of_subsingleton [h : Subsingleton E] (f : E → F) (x : E) : HasFDerivAt f (0 : E →L[𝕜] F) x :=
  by
  rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]
  exact hasFDerivWithinAt_singleton f x

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