max_max_max_comm

Mathlib.Order.Lattice

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

English

For any a, b, c, d in a linear order, max(max(a,b), max(c,d)) equals max(max(a,c), max(b,d)).

Русский

Для любых a, b, c, d в линейном порядке выполняется равенство: max(max(a,b), max(c,d)) = max(max(a,c), max(b,d)).

LaTeX

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

Lean4

theorem max_max_max_comm : max (max a b) (max c d) = max (max a c) (max b d) :=
  sup_sup_sup_comm _ _ _ _

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

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

Разделы

Аффилиация

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