min_max_distrib_left

Mathlib.Order.MinMax

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

English

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

Русский

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

LaTeX

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

Lean4

theorem min_max_distrib_left (a b c : α) : min a (max b c) = max (min a b) (min a c) :=
  inf_sup_left _ _ _

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

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

Разделы

Аффилиация

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