differentiable_fun_id

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#differentiable_fun_id

← MathLib Explorer

English

The function id, written as (fun x => x), is differentiable at every x in E.

Русский

Функция id, записанная как (fun x => x), дифференцируема в каждой точке x ∈ E.

LaTeX

$$$\mathrm{Differentiable}_{\mathbb{K}}(\lambda x: x, x)$$$

Lean4

/-- Variant with `fun x => x` rather than `id` -/
@[simp, fun_prop]
theorem differentiable_fun_id : Differentiable 𝕜 fun x : E => x := fun _ => differentiableAt_id

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru