strictly monotone functions, max, min and abs
This file proves basic properties about strictly monotone functions,
maxima and minima on a decidable_linear_order, and the absolute value
function on linearly ordered add_comm_groups, semirings and rings.
Tags
min, max, abs
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
monotone.map_max
{α : Type u}
{β : Type v}
[decidable_linear_order α]
[decidable_linear_order β]
{f : α → β}
{a b : α} :
theorem
monotone.map_min
{α : Type u}
{β : Type v}
[decidable_linear_order α]
[decidable_linear_order β]
{f : α → β}
{a b : α} :
theorem
fn_min_mul_fn_max
{α : Type u}
{β : Type v}
[decidable_linear_order α]
[comm_semigroup β]
(f : α → β)
(n m : α) :
theorem
fn_min_add_fn_max
{α : Type u}
{β : Type v}
[decidable_linear_order α]
[add_comm_semigroup β]
(f : α → β)
(n m : α) :
@[simp]
@[simp]
theorem
min_le_add_of_nonneg_right
{α : Type u}
[decidable_linear_ordered_add_comm_group α]
{a b : α} :
theorem
min_le_add_of_nonneg_left
{α : Type u}
[decidable_linear_ordered_add_comm_group α]
{a b : α} :
theorem
abs_max_sub_max_le_abs
{α : Type u}
[decidable_linear_ordered_add_comm_group α]
(a b c : α) :