Theorems · Definition · real analysis

curveIntegralFun

{𝕜 : Type u_4} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {a b : E} → (E → E →L[𝕜] F) → Path a b → ℝ → F

The function t ↦ ω (γ t) (γ' t) which appears in the definition of a curve integral. This definition is used to factor out common parts of lemmas about CurveIntegrable and curveIntegral.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Cited by

33 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace