English
If f is a binary operation on a partially ordered set and f(a,b) ≤ f(b,a) for all a,b, then f is commutative: f(a,b) = f(b,a).
Русский
Пусть f — бинарная операция на частично упорядоченном множестве и для всех a,b выполняется f(a,b) ≤ f(b,a). Тогда f коммутирует: f(a,b) = f(b,a).
LaTeX
$$$(\\forall a,b, f(a,b) \\le f(b,a)) \\Rightarrow (\\forall a,b, f(a,b) = f(b,a))$$$
Lean4
/-- To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`,
`b`. -/
theorem commutative_of_le {f : β → β → α} (comm : ∀ a b, f a b ≤ f b a) : ∀ a b, f a b = f b a := fun _ _ ↦
(comm _ _).antisymm <| comm _ _
