smul_Ici

Mathlib.Algebra.Order.Field.Pointwise

URI: https://scilib.ai/kg/mathlib#LinearOrderedField.smul_Ici

English

For r > 0, the image of the closed interval Icc a b under multiplication by r is Icc (r a) (r b).

Русский

При r>0 образ замкнутого интервала Icc(a,b) при умножении на r равен Icc(ra, rb).

LaTeX

$$$r\\cdot (I\\!\\!Icc\\ a\\ b) = I\\!\\Icc\\ (r a)\\ (r b)$$$

Lean4

theorem smul_Ici : r • Ici a = Ici (r * a) :=
  (OrderIso.mulLeft₀ r hr).image_Ici a

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

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

Разделы

Аффилиация

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