refl

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

URI: https://scilib.ai/kg/mathlib#CurveIntegrable.refl

English

The constant-path curve is curve-integrable for any ω.

Русский

Константный путь является криво интегрируемым для любой ω.

LaTeX

$$$ \\text{CurveIntegrable}(\\omega, \\mathrm{refl}(a)) $$$

Lean4

@[simp]
theorem refl (ω : E → E →L[𝕜] F) (a : E) : CurveIntegrable ω (.refl a) := by simp [CurveIntegrable, Pi.zero_def]

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

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

Разделы

Аффилиация

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