periodic_of_eq — Mathlib

English

If a global integral curve γ crosses itself at a and b, then γ is periodic with period a − b.

Русский

Если интегральная кривая γ пересекает себя в точках a и b, то γ периодична с периодом a − b.

LaTeX

$$$\gamma(a)=\gamma(b) \Rightarrow \text{Periodicity}(\gamma, a-b).$$$

Lean4

/-- For a global integral curve `γ`, if it crosses itself at `a b : ℝ`, then it is periodic with
period `a - b`. -/
theorem periodic_of_eq [BoundarylessManifold I M] (hγ : IsMIntegralCurve γ v)
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (heq : γ a = γ b) : Periodic γ (a - b) :=
  by
  intro t
  apply congrFun <| isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := b) hv (hγ.comp_add _) hγ _
  rw [comp_apply, add_sub_cancel, heq]

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