derivWithin_id — Mathlib

English

Let x ∈ 𝕜 and s ⊆ 𝕜 be such that UniqueDiffWithinAt 𝕜 s x holds. Then the derivative of the identity map within s at x equals 1.

Русский

Пусть x ∈ 𝕜 и s ⊆ 𝕜 такие, что в x существует единственная производная внутри s. Тогда производная тождественной карты внутри s в точке x равна 1.

LaTeX

$$$\frac{d}{dx} x = 1$$$

Lean4

theorem derivWithin_id (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin id s x = 1 :=
  (hasDerivWithinAt_id x s).derivWithin hxs

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