Documentation

Init.Data.Nat.MinMax

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
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 ba ca 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
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