English
For any a in a commutative monoid with a linear order, a acts on the closed interval Icc(b,c) by multiplication to give the interval Icc(ab, ac): a • Icc(b,c) = Icc(ab, ac).
Русский
Для обозначения умножения на элемент a на замкнутом интервале Icc(b,c) получаем Icc(ab, ac).
LaTeX
$$$$ a \\cdot Icc(b,c) = Icc(a b, a c). $$$$
Lean4
@[to_additive (attr := simp)]
theorem smul_Icc (a b c : α) : a • Icc b c = Icc (a * b) (a * c) :=
by
ext x
constructor
· rintro ⟨y, ⟨hby, hyc⟩, rfl⟩
exact ⟨mul_le_mul_left' hby _, mul_le_mul_left' hyc _⟩
· rintro ⟨habx, hxac⟩
obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
rwa [mul_assoc, mul_le_mul_iff_left] at hxac
