curveIntegral_segment_const — Mathlib

English

If ω is constant along a segment, then the curve integral over the concatenation of two segments equals the value at the endpoint difference, ω(b−a).

Русский

Если ω постоянна на отрезке, то интеграл по конкатенации двух отрезков равен значению ω(b−a).

LaTeX

$$$\\text{curveIntegralSegmentConst}(\\omega, a, b) : \\int_{\\text{segment}(a,b)} \\omega = \\omega(b-a)$$$

Lean4

@[simp]
theorem curveIntegral_segment_const [NormedSpace ℝ E] [CompleteSpace F] (ω : E →L[𝕜] F) (a b : E) :
    ∫ᶜ _ in .segment a b, ω = ω (b - a) :=
  by
  letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
  simp [curveIntegral_segment]

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