differentiableWithinAt_id' — Mathlib

English

Variant stating differentiability of the identity map restricted to a set s, using the identity function in the form (fun x => x).

Русский

Вариант: дифференцируемость ограниченного идентичного отображения на s, используя функцию (fun x => x).

LaTeX

$$$\operatorname{DifferentiableWithinAt}_{\mathbb{K}}(\lambda x: x, s, x)$$$

Lean4

/-- Variant with `fun x => x` rather than `id` -/
@[fun_prop]
theorem differentiableWithinAt_id' : DifferentiableWithinAt 𝕜 (fun x => x) s x :=
  differentiableWithinAt_id

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