mem_range_iff_mem_finset_range_of_mod_eq'

English

If f: ℕ → α is periodic with period n > 0, i.e., f(i mod n) = f(i) for all i, then a ∈ Set.range f iff a ∈ (Finset.range n).image f.

Русский

Если функция f: ℕ → α периодична с периодом n > 0, то для любого a: a ∈ образа f тогда, когда a ∈ образа f на Finset.range n.

LaTeX

$$$ a \\in \\operatorname{Set.range} f \\iff a \\in (\\operatorname{Finset.range} n).image f $$$

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 :=
  by
  constructor
  · rintro ⟨i, hi⟩
    simp only [mem_image, mem_range]
    exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
  · rintro h
    simp only [mem_image, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

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