map_add_right_Ico — Mathlib

English

For a locally finite order and additive commutative monoid, translating the left endpoint of the interval Ico by c preserves the interval: ((Ico a b).map (x ↦ x+c)) = Ico (a+c) (b+c).

Русский

В локально конечном порядке для аддитивной группы сохранение левой границы интервала Ico после сдвига на c даёт Ico(a+c, b+c).

LaTeX

$$$((Ico\ a\ b).\mathrm{map}(\lambda x. x+c)) = Ico(a+c, b+c)$$$

Lean4

theorem map_add_right_Ico (a b c : α) : ((Ico a b).map fun x => x + c) = Ico (a + c) (b + c) :=
  by
  simp_rw [add_comm _ c]
  exact map_add_left_Ico _ _ _

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