curveIntegrable_smul_iff — Mathlib

English

For any scalar c, CurveIntegrable (c • ω) γ holds iff either c = 0 or CurveIntegrable ω γ holds.

Русский

Для любого скаляра c утверждение о интегрируемости по кривой для c•ω эквивалентно либо c = 0, либо интегрируемости ω по γ.

LaTeX

$$$\\operatorname{CurveIntegrable}(c \\cdot \\omega, \\gamma) \\iff c = 0 \\lor \\operatorname{CurveIntegrable}(\\omega, \\gamma)$$$

Lean4

@[simp]
theorem curveIntegrable_smul_iff : CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ :=
  by
  rcases eq_or_ne c 0 with rfl | hc
  · simp [CurveIntegrable.zero]
  · simp only [hc, false_or]
    refine ⟨fun h ↦ ?_, .smul⟩
    simpa [hc] using h.smul (c := c⁻¹)

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