image_add_const_Ico

Mathlib.Algebra.Order.Interval.Set.Monoid

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

English

Constant translation by a maps the half-open interval Ico(b, c) to Ico(b + a, c + a).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_add_const_Ico : (fun x => x + a) '' Ico b c = Ico (b + a) (c + a) :=
  (Ico_add_bij _ _ _).image_eq

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

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

Разделы

Аффилиация

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