toIcoDiv_sub_eq_toIcoDiv_add — Mathlib

English

For any a, b, c, the relation toIcoDiv hp a (b − c) = toIcoDiv hp (a + c) b holds, linking subtraction to a shifted addition.

Русский

Для любых a, b, c выполняется: toIcoDiv hp a (b − c) = toIcoDiv hp (a + c) b.

LaTeX

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

Lean4

theorem toIcoDiv_sub_eq_toIcoDiv_add (a b c : α) : toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b :=
  by
  apply toIcoDiv_eq_of_sub_zsmul_mem_Ico
  rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_right_comm]
  exact sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

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