Theorems · Definition · global analysis

extDerivWithin

{𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → (E → E [⋀^Fin n]→L[𝕜] F) → Set E → E → E [⋀^Fin (n + 1)]→L[𝕜] F

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.

Defined in

Mathlib.Analysis.Calculus.DifferentialForm.Basic

Cited by

23 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace