image_add_right_Icc — Mathlib

English

Let α be an AddCommMonoid with a PartialOrder that is LocallyFinite and cancellative in addition. Then translating the right endpoint of a closed interval preserves closedness: the image of Icc(a,b) under x ↦ x+c is Icc(a+c,b+c).

Русский

Пусть α — добавочное моноид с частичным порядком; образ Icc(a,b) при x↦x+c равен Icc(a+c,b+c).

LaTeX

$$$\forall a,b,c:\alpha,\ (Icc\ a\ b).image(\lambda x. x+c) = Icc(a+c, b+c)$$$

Lean4

@[simp]
theorem image_add_right_Icc (a b c : α) : (Icc a b).image (· + c) = Icc (a + c) (b + c) := by
  rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

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