Max_and_Min_are_Associative
Provedmax-and-min-operationsproofwiki
The max and min operations are associative: max(max(x,y),z) = max(x,max(y,z)) and min(min(x,y),z) = min(x,min(y,z)).
Preamble
import Mathlib.Order.MinMax
Formal statement
theorem Max_and_Min_are_Associative {α : Type _} [LinearOrder α] (x y z : α) : max (max x y) z = max x (max y z) ∧ min (min x y) z = min x (min y z) := by sorrySource