# min lemmas #

source
theorem Nat.min_eq_min {b : Nat} (a : Nat) :
a.min b = min a b
source
@[simp]
theorem Nat.zero_min (a : Nat) :
min 0 a = 0
source
@[simp]
theorem Nat.min_zero (a : Nat) :
min a 0 = 0
source
@[simp]
theorem Nat.add_min_add_right (a b c : Nat) :
min (a + c) (b + c) = min a b + c
source
@[simp]
theorem Nat.add_min_add_left (a b c : Nat) :
min (a + b) (a + c) = a + min b c
source
@[simp]
theorem Nat.mul_min_mul_right (a b c : Nat) :
min (a * c) (b * c) = min a b * c
source
@[simp]
theorem Nat.mul_min_mul_left (a b c : Nat) :
min (a * b) (a * c) = a * min b c
source
theorem Nat.min_comm (a b : Nat) :
min a b = min b a
source
instance Nat.instCommutativeMin :
Std.Commutative min
source
theorem Nat.min_le_right (a b : Nat) :
min a b ≤ b
source
theorem Nat.min_le_left (a b : Nat) :
min a b ≤ a
source
@[simp]
theorem Nat.min_eq_left {a b : Nat} (h : a ≤ b) :
min a b = a
source
@[simp]
theorem Nat.min_eq_right {a b : Nat} (h : b ≤ a) :
min a b = b
source
theorem Nat.le_min_of_le_of_le {a b c : Nat} :
a ≤ b → a ≤ c → a ≤ min b c
source
theorem Nat.le_min {a b c : Nat} :
a ≤ min b c ↔ a ≤ b ∧ a ≤ c
source
theorem Nat.lt_min {a b c : Nat} :
a < min b c ↔ a < b ∧ a < c

# max lemmas #

source
theorem Nat.max_eq_max {b : Nat} (a : Nat) :
a.max b = max a b
source
@[simp]
theorem Nat.zero_max (a : Nat) :
max 0 a = a
source
@[simp]
theorem Nat.max_zero (a : Nat) :
max a 0 = a
source
@[simp]
theorem Nat.add_max_add_right (a b c : Nat) :
max (a + c) (b + c) = max a b + c
source
@[simp]
theorem Nat.add_max_add_left (a b c : Nat) :
max (a + b) (a + c) = a + max b c
source
@[simp]
theorem Nat.mul_max_mul_right (a b c : Nat) :
max (a * c) (b * c) = max a b * c
source
@[simp]
theorem Nat.mul_max_mul_left (a b c : Nat) :
max (a * b) (a * c) = a * max b c
source
theorem Nat.max_comm (a b : Nat) :
max a b = max b a
source
instance Nat.instCommutativeMax :
Std.Commutative max
source
theorem Nat.le_max_left (a b : Nat) :
a ≤ max a b
source
theorem Nat.le_max_right (a b : Nat) :
b ≤ max a b
source
@[simp]
theorem Nat.max_eq_right {a b : Nat} (h : a ≤ b) :
max a b = b
source
@[simp]
theorem Nat.max_eq_left {a b : Nat} (h : b ≤ a) :
max a b = a
source
theorem Nat.max_le_of_le_of_le {a b c : Nat} :
a ≤ c → b ≤ c → max a b ≤ c
source
theorem Nat.max_le {a b c : Nat} :
max a b ≤ c ↔ a ≤ c ∧ b ≤ c
source
theorem Nat.max_lt {a b c : Nat} :
max a b < c ↔ a < c ∧ b < c