MaxCut by argmin

Stream: mathlib4

[Martin Dvořák]

Is there a better way to express that argmin f is exactly {![a, b], ![b, a]} using mathlib?

def Function.HasMaxCutPropertyAt {D C : Type} [OrderedAddCommMonoid C]
    (f : (Fin 2 → D) → C) (a b : D) : Prop :=
  f ![a, b] = f ![b, a] ∧ ∀ x y : D, f ![a, b] ≤ f ![x, y] ∧
      (f ![a, b] = f ![x, y] → a = x ∧ b = y ∨ a = y ∧ b = x)