ofDual_bot

Mathlib.Order.BoundedOrder.Basic

URI: https://scilib.ai/kg/mathlib#OrderDual.ofDual_bot

English

In the dual order, the bottom maps to the top: ofDual(⊥) = ⊤.

Русский

В двойственном порядке нижняя граница сопоставляется верхней: ofDual(⊥) = ⊤.

LaTeX

$$$ \operatorname{ofDual}(\bot) = \top $$$

Lean4

@[simp]
theorem ofDual_bot [Top α] : ofDual ⊥ = (⊤ : α) :=
  rfl

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

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

Разделы

Аффилиация

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