toIocMod_apply_right — Mathlib

English

For hp, a, b, c, we have toIocMod(hp, a, b) = c iff c ∈ Ioc(a, a+p) and there exists z ∈ ℤ with b = c + z p.

Русский

Для hp, a, b, c выполняется: toIocMod(hp, a, b) = c тогда и только тогда c ∈ Ioc(a, a+p) и существует z ∈ ℤ: b = c + z p.

LaTeX

$$$$\text{toIocMod}(hp, a, b) = c \iff c \in \mathrm{Ioc}(a, a+p) \land \exists z \in \mathbb{Z},\; b = c + z p$$$$

Lean4

theorem toIocMod_apply_right (a : α) : toIocMod hp a (a + p) = a + p :=
  by
  rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]
  exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

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