max_min_distrib_right

Mathlib.Order.MinMax

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

English

In a linear order, the right distributive law holds: max(min(a, b), c) = min(max(a, c), max(b, c)).

Русский

В линейном порядке выполняется правая дистрибутивность: max(min(a, b), c) = min(max(a, c), max(b, c)).

LaTeX

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

Lean4

theorem max_min_distrib_right (a b c : α) : max (min a b) c = min (max a c) (max b c) :=
  sup_inf_right _ _ _

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

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

Разделы

Аффилиация

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