curveIntegral_refl

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

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

English

The integral of a 1-form along a constant path is zero.

Русский

Интеграл по константному пути 1-формы равен нулю.

LaTeX

$$$ \\int^{\\curvearrowleft}_{\\gamma = \\mathrm{refl}(a)} \\omega x = 0 $$$

Lean4

@[simp]
theorem curveIntegral_refl (ω : E → E →L[𝕜] F) (a : E) : ∫ᶜ x in .refl a, ω x = 0 := by simp [curveIntegral]

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

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

Разделы

Аффилиация

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