max_min_distrib_left

Mathlib.Order.MinMax

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

English

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

Русский

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

LaTeX

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

Lean4

theorem max_min_distrib_left (a b c : α) : max a (min b c) = min (max a b) (max a c) :=
  sup_inf_left _ _ _

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

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

Разделы

Аффилиация

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