map_add_right_Ico — Mathlib

English

In the same setting, translating the Ico interval by c (on the right) yields Ico(a+c,b+c).

Русский

В той же постановке переносим интервал Ico вправо на c и получаем Ico(a+c,b+c).

LaTeX

$$$\{x+c \mid x \in Ico(a,b)\} = Ico(a+c,b+c)$$$

Lean4

@[simp]
theorem map_add_right_Ico (a b c : α) : (Ico a b).map (addRightEmbedding c) = Ico (a + c) (b + c) :=
  by
  rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
  exact Set.image_add_const_Ico _ _ _

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