merge_isCommutative — Mathlib

English

If f is a commutative operation, then merging with f on options is commutative.

Русский

Если f — коммутативная операция, то объединение через merge f над опциями коммутативно.

LaTeX

$$$ [Std.Commutative\ f] \Rightarrow \mathrm{Std.Commutative} (\mathrm{Option.merge}\ f)$$$

Lean4

@[deprecated commutative_merge (since := "2025-06-03")]
theorem merge_isCommutative (f : α → α → α) [Std.Commutative f] : Std.Commutative (merge f) :=
  commutative_merge f

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