Documentation

Mathlib.Algebra.Order.Field.Pointwise

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} [LinearOrderedField K] {a b r : K} (hr : 0 < r) :
theorem LinearOrderedField.smul_Icc {K : Type u_1} [LinearOrderedField K] {a b r : K} (hr : 0 < r) :
theorem LinearOrderedField.smul_Ico {K : Type u_1} [LinearOrderedField K] {a b r : K} (hr : 0 < r) :
theorem LinearOrderedField.smul_Ioc {K : Type u_1} [LinearOrderedField K] {a b r : K} (hr : 0 < r) :