Max_and_Min_Operations_are_Distributive_over_Each_Other
Proveddistributive-operationsmax-and-min-operationsproofwiki
The max and min operations distribute over each other: max{x, min{y,z}} = min{max{x,y}, max{x,z}} and min{x, max{y,z}} = max{min{x,y}, min{x,z}}.
Preamble
import Mathlib.Order.MinMax
Formal statement
theorem Max_and_Min_Operations_are_Distributive_over_Each_Other {α : Type _} [LinearOrder α] (x y z : α) : max x (min y z) = min (max x y) (max x z) ∧ min x (max y z) = max (min x y) (min x z) := by sorrySource