left_comm

Mathlib.Order.MinMax

URI: https://scilib.ai/kg/mathlib#Max.left_comm

English

Let (α, ≤) be a linear ordered set. Then for all a, b, c ∈ α, we have max a (max b c) = max b (max a c).

Русский

Пусть (α, ≤) упорядочено линейно. Тогда для любых a, b, c ∈ α выполняется max a (max b c) = max b (max a c).

LaTeX

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

Lean4

theorem left_comm (a b c : α) : max a (max b c) = max b (max a c) := by rw [← max_assoc, max_comm a, max_assoc]

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

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

Разделы

Аффилиация

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