English
If f is a commutative binary operation and for all a,b,c we have f(f(a,b),c) ≤ f(a, f(b,c)), then f is associative.
Русский
Пусть f — коммутативная бинарная операция и для всех a,b,c выполняется f(f(a,b),c) ≤ f(a, f(b,c)). Тогда f ассоциативна.
LaTeX
$$Std.Commutative f → (∀ a b c, f(f(a,b),c) ≤ f(a, f(b,c))) → Std.Associative f$$
Lean4
/-- To prove associativity of a commutative binary operation `○`, we only to check
`(a ○ b) ○ c ≤ a ○ (b ○ c)` for all `a`, `b`, `c`. -/
theorem associative_of_commutative_of_le {f : α → α → α} (comm : Std.Commutative f)
(assoc : ∀ a b c, f (f a b) c ≤ f a (f b c)) : Std.Associative f where
assoc a b
c :=
le_antisymm (assoc _ _ _) <| by
rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
exact assoc ..
