image_add_left_Ioc

Mathlib.Algebra.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

The left-translation image of Ioc(a,b) by c is Ioc(a+c,b+c).

Русский

Граф изображения левого переноса Ioc(a,b) на c дает Ioc(a+c,b+c).

LaTeX

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

Lean4

@[simp]
theorem image_add_left_Ioc (a b c : α) : (Ioc a b).image (c + ·) = Ioc (c + a) (c + b) := by
  rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

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

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

Разделы

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

Аффилиация

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