English
If a differential form ω is sufficiently smooth at x (ContDiffAt), then the second exterior derivative at x vanishes.
Русский
Если форма ω достаточно гладкая в точке x (ContDiffAt), то вторая внешняя производная в x равна нулю.
LaTeX
$$$ h_ω : ContDiffAt 𝕜 r ω x, \\ hr : minSmoothness 𝕜 2 ≤ r \\Rightarrow extDeriv (extDeriv ω) x = 0 $$$
Lean4
/-- The second exterior derivative of a sufficiently smooth differential form is zero. -/
theorem extDeriv_extDeriv_apply (hω : ContDiffAt 𝕜 r ω x) (hr : minSmoothness 𝕜 2 ≤ r) : extDeriv (extDeriv ω) x = 0 :=
by
simp only [← extDerivWithin_univ]
apply extDerivWithin_extDerivWithin_apply (s := univ) hω.contDiffWithinAt hr <;> simp