map_add_left_Icc — Mathlib

English

For a,b,c in α, the image of the Icc interval under x ↦ x + c on the left equals Icc(a+c,b+c).

Русский

Образ Icc(a,b) под отображением x ↦ x + c слева равен Icc(a+c,b+c).

LaTeX

$$$ (Icc\ a\ b).map(\\text{addLeftEmbedding } c) = Icc( a+c, b+c) $$$

Lean4

@[simp]
theorem map_add_left_Icc (a b c : α) : (Icc a b).map (addLeftEmbedding c) = Icc (c + a) (c + b) :=
  by
  rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
  exact Set.image_const_add_Icc _ _ _

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