curveIntegral_of_not_completeSpace

English

The curve integral ω along γ is the interval integral of the curveIntegralFun ω γ over [0,1].

Русский

Кривой интеграл ω по γ равен интегралу по интервалу [0,1] функции curveIntegralFun ω γ.

LaTeX

$$$ \\curveIntegral(\\omega, \\gamma) = \\int_{0}^{1} \\curveIntegralFun(\\omega, \\gamma, t) \\, dt $$$

Lean4

/-- curve integral is defined using Bochner integral,
thus it is defined as zero whenever the codomain is not a complete space. -/
theorem curveIntegral_of_not_completeSpace (h : ¬CompleteSpace F) (ω : E → E →L[𝕜] F) (γ : Path a b) :
    ∫ᶜ x in γ, ω x = 0 := by simp [curveIntegral, intervalIntegral, integral, h]

Похожие утверждения