curveIntegrable_fun_neg_iff

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

URI: https://scilib.ai/kg/mathlib#curveIntegrable_fun_neg_iff

English

If ω is identically zero, then any path is curve-integrable with ω, and the integral is zero.

Русский

Если ω тождественно ноль, то по любой кривой интеграл по ω равен нулю.

LaTeX

$$$\\text{CurveIntegrable}(0, γ) \\text{ and } \\int_{γ} 0 = 0$$$

Lean4

@[simp]
theorem curveIntegrable_fun_neg_iff : CurveIntegrable (-ω ·) γ ↔ CurveIntegrable ω γ :=
  curveIntegrable_neg_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru