toIocDiv_sub_eq_toIocDiv_add — Mathlib

English

For any a, b, c, the identity toIocDiv hp a (b − c) = toIocDiv hp (a + c) b holds, connecting subtraction to a shifted addition.

Русский

Для любых a, b, c верна тождество toIocDiv hp a (b − c) = toIocDiv hp (a + c) b.

LaTeX

$$$\operatorname{toIocDiv}\\_{hp}\, a\\, (b - c) = \operatorname{toIocDiv}\\_{hp}\, (a + c)\\, b$$$

Lean4

theorem toIocDiv_sub_eq_toIocDiv_add (a b c : α) : toIocDiv hp a (b - c) = toIocDiv hp (a + c) b :=
  by
  apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
  rw [← sub_right_comm, Set.sub_mem_Ioc_iff_left, add_right_comm]
  exact sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

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