max_bot_left

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

Пусть α имеет нижнюю границу ⊥. Тогда максимум ⊥ и a равен a.

LaTeX

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

Lean4

theorem max_bot_left [OrderBot α] (a : α) : max ⊥ a = a :=
  bot_sup_eq _

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

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

Разделы

Аффилиация

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