HasMaxCutProperty — Mathlib

English

A fractional operation ω is associated with a max-cut property if there exist two labels a,b ∈ D, a ≠ b, such that the cost function f has the Max-Cut property at a,b, i.e., the cut determined by a,b is the unique minimizer up to swapping a and b.

Русский

Фракционная операция ω связана со свойством максимального разреза: найдутся два разных ярлыка a,b ∈ D, таких что функция затрат достигает минимума только на пары (a,b) и (b,a).

LaTeX

$$$\\exists a,b\\in D, a\\neq b \\wedge f.HasMaxCutPropertyAt a b$$$

Lean4

/-- Function `f` has Max-Cut property at some two non-identical labels. -/
def HasMaxCutProperty (f : (Fin 2 → D) → C) : Prop :=
  ∃ a b : D, a ≠ b ∧ f.HasMaxCutPropertyAt a b

Похожие утверждения