min_min_min_comm

Mathlib.Order.Lattice

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

English

For any a, b, c, d in α, min(min(a,b), min(c,d)) equals min(min(a,c), min(b,d)).

Русский

Для любых a, b, c, d в упорядоченном множестве выполнено равенство min(min(a,b), min(c,d)) = min(min(a,c), min(b,d)).

LaTeX

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

Lean4

theorem min_min_min_comm : min (min a b) (min c d) = min (min a c) (min b d) :=
  inf_inf_inf_comm _ _ _ _

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

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

Разделы

Аффилиация

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