min_top_left

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem min_top_left [OrderTop α] (a : α) : min ⊤ a = a :=
  top_inf_eq _

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

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

Разделы

Аффилиация

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