image_add_const_Ioo

Mathlib.Algebra.Order.Interval.Set.Monoid

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

English

Translation by a maps the open interval 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_add_const_Ioo : (fun x => x + a) '' Ioo b c = Ioo (b + a) (c + a) :=
  (Ioo_add_bij _ _ _).image_eq

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

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

Разделы

Аффилиация

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