smul — Mathlib

English

If h is CurveIntegrable ω γ, then h.smul: CurveIntegrable (c • ω) γ.

Русский

Если ω интегрируема по кривой, то её масштабирование скаляром также интегрируемо.

LaTeX

$$$\\text{CurveIntegrable}(\\omega, \\gamma) \\Rightarrow \\text{CurveIntegrable}(c \\cdot \\omega, \\gamma)$$$

Lean4

theorem smul (h : CurveIntegrable ω γ) : CurveIntegrable (c • ω) γ := by
  simpa [CurveIntegrable] using IntervalIntegrable.smul h c

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