mathlib documentation

algebra.order_functions

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

source
@[simp]
theorem le_min_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
c ≤ min a b ↔ c ≤ a ∧ c ≤ b

source
@[simp]
theorem max_le_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b ≤ c ↔ a ≤ c ∧ b ≤ c

source
theorem max_le_max {α : Type u} [decidable_linear_order α] {a b c d : α} (a_1 : a ≤ c) (a_2 : b ≤ d) :
max a b ≤ max c d

source
theorem min_le_min {α : Type u} [decidable_linear_order α] {a b c d : α} (a_1 : a ≤ c) (a_2 : b ≤ d) :
min a b ≤ min c d

source
theorem le_max_left_of_le {α : Type u} [decidable_linear_order α] {a b c : α} (a_1 : a ≤ b) :
a ≤ max b c

source
theorem le_max_right_of_le {α : Type u} [decidable_linear_order α] {a b c : α} (a_1 : a ≤ c) :
a ≤ max b c

source
theorem min_le_left_of_le {α : Type u} [decidable_linear_order α] {a b c : α} (a_1 : a ≤ c) :
min a b ≤ c

source
theorem min_le_right_of_le {α : Type u} [decidable_linear_order α] {a b c : α} (a_1 : b ≤ c) :
min a b ≤ c

source
theorem max_min_distrib_left {α : Type u} [decidable_linear_order α] {a b c : α} :
max a (min b c) = min (max a b) (max a c)

source
theorem max_min_distrib_right {α : Type u} [decidable_linear_order α] {a b c : α} :
max (min a b) c = min (max a c) (max b c)

source
theorem min_max_distrib_left {α : Type u} [decidable_linear_order α] {a b c : α} :
min a (max b c) = max (min a b) (min a c)

source
theorem min_max_distrib_right {α : Type u} [decidable_linear_order α] {a b c : α} :
min (max a b) c = max (min a c) (min b c)

source
theorem min_le_max {α : Type u} [decidable_linear_order α] {a b : α} :
min a b ≤ max a b

source
@[instance]
def max_idem {α : Type u} [decidable_linear_order α] :
is_idempotent α max

An instance asserting that max a a = a

source
@[instance]
def min_idem {α : Type u} [decidable_linear_order α] :
is_idempotent α min

An instance asserting that min a a = a

source
@[simp]
theorem min_le_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
min a b ≤ c ↔ a ≤ c ∨ b ≤ c

source
@[simp]
theorem le_max_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a ≤ max b c ↔ a ≤ b ∨ a ≤ c

source
@[simp]
theorem max_lt_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b < c ↔ a < c ∧ b < c

source
@[simp]
theorem lt_min_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a < min b c ↔ a < b ∧ a < c

source
@[simp]
theorem lt_max_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a < max b c ↔ a < b ∨ a < c

source
@[simp]
theorem min_lt_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
min a b < c ↔ a < c ∨ b < c

source
theorem max_lt_max {α : Type u} [decidable_linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
max a b < max c d

source
theorem min_lt_min {α : Type u} [decidable_linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
min a b < min c d

source
theorem min_right_comm {α : Type u} [decidable_linear_order α] (a b c : α) :
min (min a b) c = min (min a c) b

source
theorem max.left_comm {α : Type u} [decidable_linear_order α] (a b c : α) :
max a (max b c) = max b (max a c)

source
theorem max.right_comm {α : Type u} [decidable_linear_order α] (a b c : α) :
max (max a b) c = max (max a c) b

source
theorem monotone.map_max {α : Type u} {β : Type v} [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f (max a b) = max (f a) (f b)

source
theorem monotone.map_min {α : Type u} {β : Type v} [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f (min a b) = min (f a) (f b)

source
theorem min_choice {α : Type u} [decidable_linear_order α] (a b : α) :
min a b = a ∨ min a b = b

source
theorem max_choice {α : Type u} [decidable_linear_order α] (a b : α) :
max a b = a ∨ max a b = b

source
theorem le_of_max_le_left {α : Type u} [decidable_linear_order α] {a b c : α} (h : max a b ≤ c) :
a ≤ c

source
theorem le_of_max_le_right {α : Type u} [decidable_linear_order α] {a b c : α} (h : max a b ≤ c) :
b ≤ c

source
theorem min_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
min a b - c = min (a - c) (b - c)

source
theorem fn_min_mul_fn_max {α : Type u} {β : Type v} [decidable_linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :
(f (min n m)) * f (max n m) = (f n) * f m

source
theorem fn_min_add_fn_max {α : Type u} {β : Type v} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :
f (min n m) + f (max n m) = f n + f m

source
theorem min_add_max {α : Type u} [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
min n m + max n m = n + m

source
theorem min_mul_max {α : Type u} [decidable_linear_order α] [comm_semigroup α] (n m : α) :
(min n m) * max n m = n * m

source
theorem abs_add {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
abs (a + b) ≤ abs a + abs b

source
theorem abs_le {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :
abs a ≤ b ↔ -b ≤ a ∧ a ≤ b

source
theorem abs_lt {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :
abs a < b ↔ -b < a ∧ a < b

source
theorem lt_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :
a < abs b ↔ a < b ∨ a < -b

source
theorem abs_sub_le_iff {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

source
theorem abs_sub_lt_iff {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) < c ↔ a - b < c ∧ b - a < c

source
theorem sub_abs_le_abs_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
abs a - abs b ≤ abs (a - b)

source
theorem abs_abs_sub_le_abs_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
abs (abs a - abs b) ≤ abs (a - b)

source
theorem abs_eq {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (hb : 0 ≤ b) :
abs a = b ↔ a = b ∨ a = -b

source
@[simp]
theorem abs_eq_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :
abs a = 0 ↔ a = 0

source
theorem abs_pos_iff {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :
0 < abs a ↔ a ≠ 0

source
@[simp]
theorem abs_nonpos_iff {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :
abs a ≤ 0 ↔ a = 0

source
theorem abs_le_max_abs_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
abs b ≤ max (abs a) (abs c)

source
theorem abs_le_abs {α : Type u_1} [decidable_linear_ordered_add_comm_group α] {a b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) :
abs a ≤ abs b

source
theorem min_le_add_of_nonneg_right {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (hb : 0 ≤ b) :
min a b ≤ a + b

source
theorem min_le_add_of_nonneg_left {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (ha : 0 ≤ a) :
min a b ≤ a + b

source
theorem max_le_add_of_nonneg {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
max a b ≤ a + b

source
theorem max_zero_sub_eq_self {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :
max a 0 - max (-a) 0 = a

source
theorem abs_max_sub_max_le_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
abs (max a c - max b c) ≤ abs (a - b)

source
theorem max_sub_min_eq_abs' {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (a - b)

source
theorem max_sub_min_eq_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (b - a)

source
theorem mul_max_of_nonneg {α : Type u} [decidable_linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * max b c = max (a * b) (a * c)

source
theorem mul_min_of_nonneg {α : Type u} [decidable_linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * min b c = min (a * b) (a * c)

source
theorem max_mul_of_nonneg {α : Type u} [decidable_linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(max a b) * c = max (a * c) (b * c)

source
theorem min_mul_of_nonneg {α : Type u} [decidable_linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(min a b) * c = min (a * c) (b * c)

source
@[simp]
theorem abs_one {α : Type u} [decidable_linear_ordered_comm_ring α] :
abs 1 = 1

source
theorem max_mul_mul_le_max_mul_max {α : Type u} [decidable_linear_ordered_comm_ring α] {a d : α} (b c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) :
max (a * b) (d * c) ≤ (max a c) * max d b