min lemmas

theorem Nat.min_eq_min {b : Nat} (a : Nat) : a.min b = min a b

@[simp]

theorem Nat.zero_min (a : Nat) : min 0 a = 0

@[simp]

theorem Nat.min_zero (a : Nat) : min a 0 = 0

@[simp]

theorem Nat.add_min_add_right (a b c : Nat) : min (a + c) (b + c) = min a b + c

@[simp]

theorem Nat.add_min_add_left (a b c : Nat) : min (a + b) (a + c) = a + min b c

@[simp]

theorem Nat.mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c

@[simp]

theorem Nat.mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c

theorem Nat.min_comm (a b : Nat) : min a b = min b a

instance Nat.instCommutativeMin : Std.Commutative min

theorem Nat.min_le_right (a b : Nat) : min a b ≤ b

theorem Nat.min_le_left (a b : Nat) : min a b ≤ a

@[simp]

theorem Nat.min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a

@[simp]

theorem Nat.min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b

theorem Nat.le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c

theorem Nat.le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

theorem Nat.lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c

max lemmas

theorem Nat.max_eq_max {b : Nat} (a : Nat) : a.max b = max a b

@[simp]

theorem Nat.zero_max (a : Nat) : max 0 a = a

@[simp]

theorem Nat.max_zero (a : Nat) : max a 0 = a

@[simp]

theorem Nat.add_max_add_right (a b c : Nat) : max (a + c) (b + c) = max a b + c

@[simp]

theorem Nat.add_max_add_left (a b c : Nat) : max (a + b) (a + c) = a + max b c

@[simp]

theorem Nat.mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c

@[simp]

theorem Nat.mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c

theorem Nat.max_comm (a b : Nat) : max a b = max b a

instance Nat.instCommutativeMax : Std.Commutative max

theorem Nat.le_max_left (a b : Nat) : a ≤ max a b

theorem Nat.le_max_right (a b : Nat) : b ≤ max a b

@[simp]

theorem Nat.max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b

@[simp]

theorem Nat.max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a

theorem Nat.max_le_of_le_of_le {a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c

theorem Nat.max_le {a b c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c