curveIntegrable_symm — Mathlib

English

CurveIntegrable is symmetric with respect to path reversal: CurveIntegrable ω γ ↔ CurveIntegrable ω γ.symm.

Русский

Симметрия CurveIntegrable при развороте пути: CurveIntegrable ω γ ↔ CurveIntegrable ω γ.symm.

LaTeX

$$$ \\text{CurveIntegrable}(\\omega, \\gamma) \\iff \\text{CurveIntegrable}(\\omega, \\gamma^{\\mathrm{symm}}) $$$

Lean4

@[simp]
theorem curveIntegrable_symm : CurveIntegrable ω γ.symm ↔ CurveIntegrable ω γ :=
  ⟨fun h ↦ by simpa using h.symm, .symm⟩

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