image_add_right_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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