Ico_eq_locus_Ioc_eq_iUnion_Ioo — Mathlib

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]

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