image_const_add_Ioo

Mathlib.Algebra.Order.Interval.Set.Monoid

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

English

Left translation by a maps Ioo(b, c) to Ioo(b + a, c + a).

Русский

Левый перенос на a переводит Ioo(b, c) в Ioo(b + a, c + a).

LaTeX

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

Lean4

@[simp]
theorem image_const_add_Ioo : (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Ioo]

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

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

Разделы

Аффилиация

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