English
If f : ℤ → α is periodic with period n > 0 and f(i mod n) = f(i) for all integers i, then a ∈ Set.range f iff a ∈ (Finset.range n).image (fun i => f i.cast).
Русский
Если f: ℤ → α периодична с периодом n > 0 и выполняется f(i mod n) = f(i) для всех целых i, то a ∈ образа f тогда и только тогда, когда a ∈ образа f на Finset.range n с использованием приведения i к натуральному.
LaTeX
$$$ a \\in \\operatorname{Set.range} f \\iff a \\in (\\operatorname{Finset.range} n).image (\\lambda i: f i.cast) $$$
Lean4
theorem mem_range_iff_mem_finset_range_of_mod_eq [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ} (hn : 0 < n)
(h : ∀ i, f (i % n) = f i) : a ∈ Set.range f ↔ a ∈ (Finset.range n).image (fun (i : ℕ) => f i) :=
suffices (∃ i, f (i % n) = a) ↔ ∃ i, i < n ∧ f ↑i = a by simpa [h]
have hn' : 0 < (n : ℤ) := Int.ofNat_lt.mpr hn
Iff.intro
(fun ⟨i, hi⟩ =>
have : 0 ≤ i % ↑n := Int.emod_nonneg _ (ne_of_gt hn')
⟨Int.toNat (i % n), by rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]; exact ⟨Int.emod_lt_of_pos i hn', hi⟩⟩)
fun ⟨i, hi, ha⟩ => ⟨i, by rw [Int.emod_eq_of_lt (Int.ofNat_zero_le _) (Int.ofNat_lt_ofNat_of_lt hi), ha]⟩
