extDeriv_constOfIsEmpty — Mathlib

English

The extDeriv of a constant-of-empty 0-form equals the corresponding linear map given by fderiv.

Русский

extDeriv константной нулевой формы равен линейному отображению, заданному fderiv.

LaTeX

$$$extDeriv (fun x => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) x = .ofSubsingleton _ _ _ (0 : Fin 1) (fderiv 𝕜 f x)$$$

Lean4

/-- The exterior derivative of a `0`-form given by a function `f`
is the 1-form given by the derivative of `f`. -/
theorem extDeriv_constOfIsEmpty (f : E → F) (x : E) :
    extDeriv (fun x ↦ constOfIsEmpty 𝕜 E (Fin 0) (f x)) x = .ofSubsingleton _ _ _ (0 : Fin 1) (fderiv 𝕜 f x) := by
  simp [← extDerivWithin_univ, extDerivWithin_constOfIsEmpty, fderivWithin_univ]

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