image_add_left_Ioo — Mathlib

English

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

Русский

Пусть α — добавочное абелева моноида с частичным порядком и локальной конечностью, допускающая отмену сложения. Смещение левой границы открытого интервала сохраняет открытость: образ Ioo(a,b) при x↦c+x равен Ioo(a+c,b+c).

LaTeX

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

Lean4

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

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