English
The set of b such that toIcoMod hp a b = toIocMod hp a b equals the union over all integers z of the open intervals Ioo(a + z p, a + p + z p).
Русский
Множество b such, что toIcoMod hp a b = toIocMod hp a b, равно объединению по всем целым z интервалов Ioo(a + z p, a + p + z p).
LaTeX
$$$ \\{ b \\mid toIcoMod hp a b = toIocMod hp a b \\} = \\bigcup_{z \\in \\mathbb{Z}} \\mathrm{Ioo}(a + z p,\ a + p + z p) $$$
Lean4
theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo :
{b | toIcoMod hp a b = toIocMod hp a b} = ⋃ z : ℤ, Set.Ioo (a + z • p) (a + p + z • p) :=
by
ext1
simp_rw [Set.mem_setOf, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ← not_modEq_iff_toIcoMod_eq_toIocMod,
modEq_iff_forall_notMem_Ioo_mod hp, not_forall, Classical.not_not]