curveIntegrable_neg_iff — Mathlib

English

The equivalence between the curve integrability of ω and its negation along γ holds as a simp lemma.

Русский

Эквивалентность интегрируемости кривой ω и −ω сохраняется как лемма-упрощение.

LaTeX

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

Lean4

@[simp]
theorem curveIntegrable_neg_iff : CurveIntegrable (-ω) γ ↔ CurveIntegrable ω γ :=
  ⟨fun h ↦ by simpa using h.neg, .neg⟩

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