extDeriv_extDeriv — Mathlib

English

If ω is sufficiently smooth on a neighborhood (ContDiff) and the smoothness bound is reached, then the second exterior derivative of ω is identically zero as a function.

Русский

Если ω достаточно гладкая на окрестности, и порог гладкости достигнут, то вторая внешняя производная ω тождественно равна нулю как функция.

LaTeX

$$$ h : ContDiff 𝕜 r ω, \\ hr : minSmoothness 𝕜 2 ≤ r \\Rightarrow extDeriv (extDeriv ω) = 0 $$$

Lean4

/-- The second exterior derivative of a sufficiently smooth differential form is zero. -/
theorem extDeriv_extDeriv (h : ContDiff 𝕜 r ω) (hr : minSmoothness 𝕜 2 ≤ r) : extDeriv (extDeriv ω) = 0 :=
  funext fun _ ↦ extDeriv_extDeriv_apply h.contDiffAt hr

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