min_bot_left

Mathlib.Order.BoundedOrder.Lattice

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

English

Let α be a type with a bottom element. For any a ∈ α, infimum of ⊥ and a equals ⊥; i.e., ⊥ ⊓ a = ⊥.

Русский

Пусть α — множество с нижней границей ⊥. Тогда для любого a ∈ α выполнено ⊥ ⊓ a = ⊥.

LaTeX

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

Lean4

theorem min_bot_left [OrderBot α] (a : α) : min ⊥ a = ⊥ :=
  bot_inf_eq _

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

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

Разделы

Аффилиация

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