extDeriv_extDeriv_apply — Mathlib

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

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