image_const_add_Ioi

Mathlib.Algebra.Order.Interval.Set.Monoid

URI: https://scilib.ai/kg/mathlib#Set.image_const_add_Ioi

English

Translation by a from the left sends the open ray Ioi b to Ioi(b + a).

Русский

Сдвиг слева на a отображает луч Ioi b в Ioi(b + a).

LaTeX

$$$(b, \infty) + a = (b + a, \infty)$$$

Lean4

@[simp]
theorem image_const_add_Ioi : (fun x => a + x) '' Ioi b = Ioi (a + b) := by simp only [add_comm a, image_add_const_Ioi]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru