instAssociativeMax

Mathlib.Order.MinMax

URI: https://scilib.ai/kg/mathlib#instAssociativeMax

English

The operation max is associative: max(max(a,b), c) = max(a, max(b,c)).

Русский

Операция max ассоциативна: max(max(a,b), c) = max(a, max(b,c)).

LaTeX

$$$ \max(\max(a,b), c) = \max(a, \max(b,c)) $$$

Lean4

instance instAssociativeMax : Std.Associative (α := α) max where assoc := max_assoc

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

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

Разделы

Аффилиация

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