merge_isAssociative

Mathlib.Data.Option.Defs

URI: https://scilib.ai/kg/mathlib#Option.merge_isAssociative

← MathLib Explorer

English

If f is associative, then merge f is associative on options.

Русский

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

LaTeX

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

Lean4

@[deprecated associative_merge (since := "2025-06-03")]
theorem merge_isAssociative (f : α → α → α) [Std.Associative f] : Std.Associative (merge f) :=
  associative_merge f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru