image_const_add_Icc

Mathlib.Algebra.Order.Interval.Set.Monoid

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

English

Translation by a from the left sends the closed interval Icc(b, c) to Icc(b + a, c + a).

Русский

Сдвиг слева на a переводит Icc(b, c) в Icc(b + a, c + a).

LaTeX

$$$Icc(b,c) + a = Icc(b+a,c+a)$$$

Lean4

@[simp]
theorem image_const_add_Icc : (fun x => a + x) '' Icc b c = Icc (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Icc]

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

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

Разделы

Аффилиация

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