mathlib documentation

algebra.order.pointwise

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) :
r set.Ioo a b = set.Ioo (r a) (r b)
theorem linear_ordered_field.smul_Icc {K : Type u_1} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Icc a b = set.Icc (r a) (r b)
theorem linear_ordered_field.smul_Ico {K : Type u_1} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Ico a b = set.Ico (r a) (r b)
theorem linear_ordered_field.smul_Ioc {K : Type u_1} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Ioc a b = set.Ioc (r a) (r b)
theorem linear_ordered_field.smul_Ioi {K : Type u_1} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Ioi a = set.Ioi (r a)
theorem linear_ordered_field.smul_Iio {K : Type u_1} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Iio a = set.Iio (r a)
theorem linear_ordered_field.smul_Ici {K : Type u_1} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Ici a = set.Ici (r a)
theorem linear_ordered_field.smul_Iic {K : Type u_1} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Iic a = set.Iic (r a)