toIcoMod_apply_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem toIcoMod_apply_right (a : α) : toIcoMod hp a (a + p) = a :=
  by
  rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]
  exact ⟨lt_add_of_pos_right _ hp, 1, by simp⟩

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