English
Let f: α → α and g: β → β. For a ∈ α and b ∈ β and a natural number n, the point (a, b) is periodic for Prod.map f g with period n if and only if a is periodic for f with period n and b is periodic for g with period n.
Русский
Пусть f: α → α и g: β → β. Для a ∈ α и b ∈ β и натурального числа n: точка (a, b) периодична для отображения Prod.map f g с периодом n тогда и только тогда, когда a периодична для f с периодом n и b периодична для g с периодом n.
LaTeX
$$$ \\mathrm{IsPeriodicPt}\\,(\\mathrm{Prod.map}\\ f\\ g)\, n\\ (a,b) \\;\\iff\\; \\mathrm{IsPeriodicPt}\\ f\\ n\\ a \\land \\mathrm{IsPeriodicPt}\\ g\\ n\\ b $$$
Lean4
@[simp]
theorem isPeriodicPt_prodMap (x : α × β) :
IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2 := by simp [IsPeriodicPt]
