min_pair

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.min_pair

English

The minimum of {a,b} is the minimum of a and b.

Русский

Минимум множества {a,b} равен min(a,b).

LaTeX

$$$\min\{a,b\} = \min(a,b)$$$

Lean4

theorem min_pair (a b : α) : Finset.min { a, b } = min (↑a) (↑b) := by simp

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

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

Разделы

Аффилиация

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