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