image_add_left_Ico

Mathlib.Algebra.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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