neg — Mathlib

English

If a curve ω is integrable along γ, then the curve integrable form −ω along γ as well.

Русский

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

LaTeX

$$$\\text{CurveIntegrable}(−ω, γ) \\Rightarrow \\text{CurveIntegrable}(ω, γ)$$$

Lean4

theorem neg (h : CurveIntegrable ω γ) : CurveIntegrable (-ω) γ := by
  simpa [CurveIntegrable] using IntervalIntegrable.neg h

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