add — Mathlib

English

If a curve is integrable with respect to ω1 and ω2, then it is integrable with respect to ω1 + ω2.

Русский

Если по кривой интегрируемость существует для ω1 и ω2, то существует для ω1 + ω2.

LaTeX

$$$\\text{CurveIntegrable}(ω_1, γ) \\to \\text{CurveIntegrable}(ω_2, γ) \\Rightarrow \\text{CurveIntegrable}(ω_1 + ω_2, γ)$$$

Lean4

protected theorem add (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : CurveIntegrable (ω₁ + ω₂) γ := by
  simpa [CurveIntegrable] using IntervalIntegrable.add h₁ h₂

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