English
For any a,b integers and v, the x in Ioc a b with x ≡ v mod r equals x in Ioc (a−v) (b−v) with r | x, mapped by adding v.
Русский
Для любых a,b ∈ ℤ и v: x ∈ Ioc a b, x ≡ v (mod r) эквивалентно x ∈ Ioc(a−v)(b−v) с r | x, отображённому на x+v.
LaTeX
$$$$ \{x\in Ioc(a,b)\mid x \equiv v\,[ZMOD\, r]\} = \{x\in Ioc(a-v,b-v)\mid r\mid x\}.map\langle(\cdot+v),\; \text{add_left_injective } v\rangle.$$$$
Lean4
theorem Ioc_filter_modEq_eq (v : ℤ) :
{x ∈ Ioc a b | x ≡ v [ZMOD r]} = {x ∈ Ioc (a - v) (b - v) | r ∣ x}.map ⟨(· + v), add_left_injective v⟩ :=
by
ext x
simp_rw [mem_map, mem_filter, mem_Ioc, 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]
