fderivWithin_fst — Mathlib

English

Let s be a set in E × F with the unique-diff Within property at p. Then the derivative within s of the first projection at p is the first projection map.

Русский

Пусть s ⊆ E × F обладает свойством уникальной точки дифференцируемости в p. Тогда производная внутри s от fst в p равна проекции fst.

LaTeX

$$$ fderivWithin 𝕜 Prod.fst s p = fst 𝕜 E F $$$

Lean4

theorem fderivWithin_fst {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) : fderivWithin 𝕜 Prod.fst s p = fst 𝕜 E F :=
  hasFDerivWithinAt_fst.fderivWithin hs

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