map_add_right_Ioo

Mathlib.Algebra.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.map_add_right_Ioo

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\{x+c \mid x \in Ioo(a,b)\} = Ioo(a+c,b+c)$$$

Lean4

@[simp]
theorem map_add_right_Ioo (a b c : α) : (Ioo a b).map (addRightEmbedding c) = Ioo (a + c) (b + c) :=
  by
  rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
  exact Set.image_add_const_Ioo _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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