English
The extDeriv within a set of a zero-form given by constOfIsEmpty agrees with the corresponding representation-built form.
Русский
extDeriv внутри множества нулевой формы, заданной constOfIsEmpty, совпадает с соответствующей формой.
LaTeX
$$$extDerivWithin (fun x => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) s x = .ofSubsingleton _ _ _ (0 : Fin 1) (fderivWithin 𝕜 f s x).$$$
Lean4
/-- The exterior derivative of a `0`-form given by a function `f` within a set
is the 1-form given by the derivative of `f` within the set. -/
theorem extDerivWithin_constOfIsEmpty (f : E → F) (hs : UniqueDiffWithinAt 𝕜 s x) :
extDerivWithin (fun x ↦ constOfIsEmpty 𝕜 E (Fin 0) (f x)) s x =
.ofSubsingleton _ _ _ (0 : Fin 1) (fderivWithin 𝕜 f s x) :=
by
simp only [extDerivWithin, ← constOfIsEmptyLIE_apply, ← Function.comp_def _ f,
(constOfIsEmptyLIE 𝕜 E F (Fin 0)).comp_fderivWithin hs, alternatizeUncurryFin_constOfIsEmptyLIE_comp]
