map_add_left_Ioc

Mathlib.Algebra.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

Translation by c on the left carries Ioc(a,b) to Ioc(a+c,b+c).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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