prodMap — Mathlib

English

If a is periodic for f with period n and b is periodic for g with period n, then (a, b) is periodic for Prod.map f g with period n.

Русский

Если a периодична относительно f с периодом n и b периодична относительно g с периодом n, тогда (a, b) периодична относительно Prod.map f g с периодом n.

LaTeX

$$$ \\mathrm{IsPeriodicPt}\\ f\\ n\\ a \\land \\mathrm{IsPeriodicPt}\\ g\\ n\\ b \\Rightarrow \\mathrm{IsPeriodicPt}\\ (\\mathrm{Prod.map}\\ f\\ g)\\ n\\ (a,b) $$$

Lean4

theorem prodMap (ha : IsPeriodicPt f n a) (hb : IsPeriodicPt g n b) : IsPeriodicPt (Prod.map f g) n (a, b) :=
  (isPeriodicPt_prodMap _).mpr ⟨ha, hb⟩

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