English
For any a,b integers and r ≠ 0, the x in Ico a b with x ≡ v mod r equals x in Ico (a−v) (b−v) with r | x, mapped by adding v.
Русский
Для любых a,b ∈ ℤ и r ≠ 0 множество x ∈ Ico a b с x ≡ v (mod r) эквивалентно множеству x ∈ Ico(a−v)(b−v) с r | x, отображённому порядком x ↦ x+v.
LaTeX
$$$$ \{x\in Ico(a,b)\mid x \equiv v\,[ZMOD\, r]\} = \{x\in Ico(a-v,b-v)\mid r\mid x\}.map\langle(\cdot+v),\; \text{add_left_injective } v\rangle.$$$$
Lean4
theorem Ico_filter_modEq_eq (v : ℤ) :
{x ∈ Ico a b | x ≡ v [ZMOD r]} = {x ∈ Ico (a - v) (b - v) | r ∣ x}.map ⟨(· + v), add_left_injective v⟩ :=
by
ext x
simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq, exists_eq_right, modEq_comm,
modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
