sub — Mathlib

English

If ω1 and ω₂ are curve-integrable along γ, then their difference ω1 − ω₂ is also curve-integrable along γ.

Русский

Если ω1 и ω₂ интегрируемы по кривой вдоль γ, то и разность ω1 − ω₂ интегрируема по той же кривой.

LaTeX

$$$\\text{CurveIntegrable}(\\omega_1 - \\omega_2, \\gamma)$$$

Lean4

protected theorem sub (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : CurveIntegrable (ω₁ - ω₂) γ :=
  sub_eq_add_neg ω₁ ω₂ ▸ h₁.add h₂.neg

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