min lemmas

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

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

instance Nat.instCommutativeMin : Std.Commutative min

Equations

• Nat.instCommutativeMin = ⋯

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

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

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

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

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

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

theorem Nat.lt_min {a : Nat} {b : Nat} {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

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

instance Nat.instCommutativeMax : Std.Commutative max

Equations

• Nat.instCommutativeMax = ⋯

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

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