English
Under NoZeroSMulDivisors on ℤ M, with hfx and hgy as above and hgxfy = f y g x = 4, the range of iterates of the composed reflection is infinite if and only if f y · x ≠ 2 · y.
Русский
При NoZeroSMulDivisors на ℤ M и условиях hfx, hgy и hgxfy = 4, множество значений спектра итераций композиции отражений бесконечно, если и только если f y · x ≠ 2 · y.
LaTeX
$$$[NoZeroSMulDivisors\\ \\mathbb{Z}\\ M]\\ (hfx:\\ f x=2)\\ (hgy:\\ g y=2)\\ (hgxfy:\\ f y\\cdot g x =4)\\Rightarrow\\n\\mathrm{range}\\;((reflection hgy)\\circ\\mathrm{trans}(reflection hfx))^{[n]} y\\text{ is infinite }\\iff f(y)\\cdot x \\neq 2\\cdot y$$$
Lean4
theorem infinite_range_reflection_reflection_iterate_iff [NoZeroSMulDivisors ℤ M] (hfx : f x = 2) (hgy : g y = 2)
(hgxfy : f y * g x = 4) :
(range <| fun n ↦ ((reflection hgy).trans (reflection hfx))^[n] y).Infinite ↔ f y • x ≠ (2 : R) • y := by
simp only [reflection_reflection_iterate hfx hgy hgxfy, infinite_range_add_nsmul_iff, sub_ne_zero]
