Pointwise operations on ordered algebraic objects #
This file contains lemmas about the effect of pointwise operations on sets with an order structure.
theorem
linear_ordered_field.smul_Ioo
{K : Type u_1}
[linear_ordered_field K]
{a b r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Icc
{K : Type u_1}
[linear_ordered_field K]
{a b r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Ico
{K : Type u_1}
[linear_ordered_field K]
{a b r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Ioc
{K : Type u_1}
[linear_ordered_field K]
{a b r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Ioi
{K : Type u_1}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Iio
{K : Type u_1}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Ici
{K : Type u_1}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Iic
{K : Type u_1}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :