min_bot_right

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem min_bot_right [OrderBot α] (a : α) : min a ⊥ = ⊥ :=
  inf_bot_eq _

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

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

Разделы

Аффилиация

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