map_add_left_Ico — Mathlib

English

Let α be a locally finite ordered cancellative additive monoid. For all a,b,c in α, translating the half-open interval Ico(a,b) by c yields the interval Ico(a+c,b+c).

Русский

Пусть α — локально конечный упорядоченный отменимый аддитивный моноид. Для любых a,b,c ∈ α сдвигом на c полузакрытого интервала Ico(a,b) получаем интервал Ico(a+c,b+c).

LaTeX

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

Lean4

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

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