max'_pair

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.max'_pair

English

For two elements a and b, the maximum of {a, b} equals max(a, b).

Русский

Для двух элементов a и b максимум множества {a, b} равен max(a,b).

LaTeX

$$$\\max'\\{a,b\\} (\\text{insert\\_nonempty} \\_ ) = \\max(a,b).$$$

Lean4

theorem max'_pair (a b : α) : max' { a, b } (insert_nonempty _ _) = max a b := by simp

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

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

Разделы

Аффилиация

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