multiset_Ico_map_mod — Mathlib

English

General version: for natural numbers n and a, the image of Ico(n, n+a) under x ↦ x mod a equals range(a).

Русский

Обобщённая версия: для naturals n и a образ Ico(n, n+a) при x mod a равен диапазону a.

LaTeX

$$$\\forall n,a\\ (Ico(n, n+a)).image (\\lambda x, x \\bmod a) = \\mathrm{range}\\ a$$$

Lean4

theorem multiset_Ico_map_mod (n a : ℕ) : (Multiset.Ico n (n + a)).map (· % a) = Multiset.range a :=
  by
  convert congr_arg Finset.val (image_Ico_mod n a)
  refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm
  exact mod_injOn_Ico _ _

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