image_mul_right_Ico

Mathlib.Algebra.Order.Group.Pointwise.Interval

URI: https://scilib.ai/kg/mathlib#Set.image_mul_right_Ico

English

The image of Ico(a,b) under right-multiplication by c is Ico(a c, b c).

Русский

Образ Ico(a,b) при правом умножении на c есть Ico(ac, bc).

LaTeX

$$$(\cdot * c) '' Ico a b = Ico(a c, b c)$$$

Lean4

theorem image_mul_right_Ico (a b : G₀) (h : 0 < c) : (fun x => x * c) '' Ico a b = Ico (a * c) (b * c) :=
  (OrderIso.mulRight₀ c h).image_Ico a b

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

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

Разделы

Аффилиация

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