Pointwise operations on ordered algebraic objects

This file contains lemmas about the effect of pointwise operations on sets with an order structure.

theorem LinearOrderedField.smul_Ioo {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b r : K} (hr : 0 < r) : r • Set.Ioo a b = Set.Ioo (r * a) (r * b)

theorem LinearOrderedField.smul_Icc {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b r : K} (hr : 0 < r) : r • Set.Icc a b = Set.Icc (r * a) (r * b)

theorem LinearOrderedField.smul_Ico {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b r : K} (hr : 0 < r) : r • Set.Ico a b = Set.Ico (r * a) (r * b)

theorem LinearOrderedField.smul_Ioc {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b r : K} (hr : 0 < r) : r • Set.Ioc a b = Set.Ioc (r * a) (r * b)

theorem LinearOrderedField.smul_Ioi {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a r : K} (hr : 0 < r) : r • Set.Ioi a = Set.Ioi (r * a)

theorem LinearOrderedField.smul_Iio {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a r : K} (hr : 0 < r) : r • Set.Iio a = Set.Iio (r * a)

theorem LinearOrderedField.smul_Ici {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a r : K} (hr : 0 < r) : r • Set.Ici a = Set.Ici (r * a)

theorem LinearOrderedField.smul_Iic {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a r : K} (hr : 0 < r) : r • Set.Iic a = Set.Iic (r * a)