max_top_left

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem max_top_left [OrderTop α] (a : α) : max ⊤ a = ⊤ :=
  top_sup_eq _

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

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

Разделы

Аффилиация

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