curveIntegrable_cast_iff — Mathlib

English

CurveIntegrable ω (γ.cast hc hd) is equivalent to CurveIntegrable ω γ when hc and hd hold.

Русский

CurveIntegrable ω (γ.cast hc hd) эквивалентно CurveIntegrable ω γ при hc hd.

LaTeX

$$$ \\text{CurveIntegrable}(\\omega, γ^{\\mathrm{cast}}) \\iff \\text{CurveIntegrable}(\\omega, γ) $$$

Lean4

@[simp]
theorem curveIntegrable_cast_iff (hc : c = a) (hd : d = b) : CurveIntegrable ω (γ.cast hc hd) ↔ CurveIntegrable ω γ :=
  by simp [CurveIntegrable]

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