English
The exterior derivative within a set of a zero-form given by a constant map coincides with the corresponding linear equivalence image of the one-derivative of f.
Русский
Внутренний производный нулевой формы, заданной константной картой, совпадает с образом соответствующего линейного отображения производной f.
LaTeX
$$$\forall f: E\to F, \; extDerivWithin (fun x \mapsto ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) \; s = .ofSubsingleton _ _ _ (0 : Fin 1) (fderivWithin 𝕜 f s x).$$$
Lean4
/-- Exterior derivative of a differential form within a set.
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 `extDerivWithin_apply`.
-/
noncomputable def extDerivWithin (ω : E → E [⋀^Fin n]→L[𝕜] F) (s : Set E) (x : E) : E [⋀^Fin (n + 1)]→L[𝕜] F :=
.alternatizeUncurryFin (fderivWithin 𝕜 ω s x)
