min_top_right

Mathlib.Order.BoundedOrder.Lattice

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

English

Let α be a linear order with a top element ⊤. Then min(a, ⊤) = a for every a ∈ α.

Русский

Пусть α имеет верхнюю границу ⊤. Тогда минимум a и ⊤ равен a для любого a.

LaTeX

$$$\\min(a, \\top) = a$$$

Lean4

theorem min_top_right [OrderTop α] (a : α) : min a ⊤ = a :=
  inf_top_eq _

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

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

Разделы

Аффилиация

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