image_add_right_Ioc — Mathlib

English

Let α be an AddCommMonoid with a PartialOrder that is LocallyFinite and cancellative in addition. Then translating the right endpoint of a half-open interval preserves the half-open form: (Ioc a b).image (· + c) = Ioc (a+c) (b+c).

Русский

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

LaTeX

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

Lean4

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

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