merge_isIdempotent — Mathlib

English

If f is an idempotent operation, then merge f is idempotent on options.

Русский

Если f идемпотентна, то merge f идемпотентна над опциями.

LaTeX

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

Lean4

@[deprecated idempotentOp_merge (since := "2025-06-03")]
theorem merge_isIdempotent (f : α → α → α) [Std.IdempotentOp f] : Std.IdempotentOp (merge f) :=
  idempotentOp_merge f

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