sub — Mathlib

English

If x has periods m and n for f, then x has period m − n (with zero when n > m).

Русский

Если x имеет периоды m и n для f, то x имеет период m − n (если n > m, то 0).

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f n x \to IsPeriodicPt f (m - n) x$$$

Lean4

protected theorem sub (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m - n) x :=
  by
  rcases le_total n m with h | h
  · refine left_of_add ?_ hn
    rwa [tsub_add_cancel_of_le h]
  · rw [tsub_eq_zero_iff_le.mpr h]
    apply isPeriodicPt_zero

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