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