toIcoMod_le_toIocMod — Mathlib

English

For any a,b the IcoMod value is not greater than the corresponding IocMod value: toIcoMod hp a b ≤ toIocMod hp a b.

Русский

Для любых a,b значение IcoMod не превосходит соответствующее значение IocMod: toIcoMod hp a b ≤ toIocMod hp a b.

LaTeX

$$$ toIcoMod\\ hp\\ a\\ b \\leq toIocMod\\ hp\\ a\\ b $$$

Lean4

theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b :=
  by
  rw [toIcoMod, toIocMod, sub_le_sub_iff_left]
  exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

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