extDerivWithin_extDerivWithin_eqOn

English

A variant of zero-second-derivative result for when ω is adequately smooth; the same vanishing conclusion holds.

Русский

Вариант нуля второго производного при достаточной гладкости; результат сохраняется.

LaTeX

$$$ h_ω : ContDiffWithinAt 𝕜 r ω s, \\ hr : minSmoothness 𝕜 2 ≤ r \\Rightarrow extDerivWithin (extDerivWithin ω s) s x = 0 $$$

Lean4

/-- The second exterior derivative of a sufficiently smooth differential form is zero. -/
theorem extDerivWithin_extDerivWithin_eqOn (hω : ContDiffOn 𝕜 r ω s) (hr : minSmoothness 𝕜 2 ≤ r)
    (hs : UniqueDiffOn 𝕜 s) : EqOn (extDerivWithin (extDerivWithin ω s) s) 0 (s ∩ closure (interior s)) :=
  by
  rintro x ⟨h'x, hx⟩
  exact extDerivWithin_extDerivWithin_apply (hω.contDiffWithinAt h'x) hr hs hx h'x

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