English
The exterior derivative within a set agrees with the exterior derivative on the whole space when restricted to the whole space.
Русский
Внутренний производный внутри полного множества совпадает с внешним (вне зависимости от определения) на всём пространстве.
LaTeX
$$$\text{extDerivWithin}(ω, s, x) = \text{extDeriv}(ω, x) \quad\text{when } s = \text{univ}. $$$
Lean4
/-- Exterior derivative of a differential form.
There are a few competing definitions of the exterior derivative of a differential form
that differ from each other by a normalization factor.
We use the following one:
$$
dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i
$$
where $$\widehat{v_i}$$ means that we omit this element of the tuple, see `extDeriv_apply`.
-/
noncomputable def extDeriv (ω : E → E [⋀^Fin n]→L[𝕜] F) (x : E) : E [⋀^Fin (n + 1)]→L[𝕜] F :=
.alternatizeUncurryFin (fderiv 𝕜 ω x)
