image_mul_left_Ico

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

Let a > 0. Left multiplication by a takes Ico(b, c) to Ico(a b, a c).

Русский

Пусть a > 0. Левое умножение на a отправляет Ico(b, c) в Ico(a b, a c).

LaTeX

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

Lean4

theorem image_mul_left_Ico (h : 0 < a) (b c : G₀) : (a * ·) '' Ico b c = Ico (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Ico b c

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

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

Разделы

Аффилиация

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