curveIntegralFun_fun_zero — Mathlib

English

For a fixed ω and segment from a to b, curve integrability along the segment is equivalent to the interval integrability of the line-map expression over [0,1].

Русский

Для фиксированного ω интегрируемость по сегменту от a до b эквивалентна интегрируемости по интервалу функции t ↦ ω(lineMap(a,b,t))(b−a) на [0,1].

LaTeX

$$$\\text{CurveIntegrable}(ω,\\text{segment}(a,b)) \\iff \\text{IntervalIntegrable}(t \\mapsto ω(\\text{lineMap}(a,b,t))(b-a),\\text{volume},0,1)$$$

Lean4

@[simp]
theorem curveIntegralFun_fun_zero : curveIntegralFun (fun _ ↦ 0 : E → E →L[𝕜] F) γ = 0 :=
  curveIntegralFun_zero

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