instAssociativeMin

Mathlib.Order.MinMax

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

English

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

Русский

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

LaTeX

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

Lean4

instance instAssociativeMin : Std.Associative (α := α) min where assoc := min_assoc

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

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

Разделы

Аффилиация

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