isLeast_pair

Mathlib.Order.Bounds.Basic

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

English

In a linear order, the least upper bound of two elements a and b is min(a,b).

Русский

В линейном порядке наименьшая верхняя граница двух элементов a и b равна min(a,b).

LaTeX

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

Lean4

theorem isLeast_pair [LinearOrder γ] {a b : γ} : IsLeast { a, b } (min a b) :=
  isLeast_singleton.insert _

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

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

Разделы

Аффилиация

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