map_add_right_Ioc

Mathlib.Algebra.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_add_right_Ioc (a b c : α) : (Ioc a b).map (addRightEmbedding c) = Ioc (a + c) (b + c) :=
  by
  rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
  exact Set.image_add_const_Ioc _ _ _

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

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

Разделы

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

Аффилиация

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