max_bot_right

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem max_bot_right [OrderBot α] (a : α) : max a ⊥ = a :=
  sup_bot_eq _

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

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

Разделы

Аффилиация

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