image_add_const_Ioc

Mathlib.Algebra.Order.Interval.Set.Monoid

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

English

Translation by a maps the half-open interval Ioc(b, c) to Ioc(b + a, c + a).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_add_const_Ioc : (fun x => x + a) '' Ioc b c = Ioc (b + a) (c + a) :=
  (Ioc_add_bij _ _ _).image_eq

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

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

Разделы

Аффилиация

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