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

/-- Variant with `fun x => x` rather than `id` -/
theorem derivWithin_id' (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (fun x => x) s x = 1 :=
  derivWithin_id x s hxs

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