merge_isId — Mathlib

English

There is a lawful identity element for merge f with none; none acts as a neutral element for merge.

Русский

Для merge f существует нейтральный элемент, равный none; none является нейтральным элементом для объединения.

LaTeX

$$$ \mathrm{Std.LawfulIdentity} (\mathrm{Option.merge}\ f) \mathrm{none}$$$

Lean4

@[deprecated lawfulIdentity_merge (since := "2025-06-03")]
theorem merge_isId (f : α → α → α) : Std.LawfulIdentity (merge f) none :=
  lawfulIdentity_merge f

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