isTop_ofDual_iff

Mathlib.Order.Max

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

English

In the dual order, the top element of toDual corresponds to the bottom in the original order.

Русский

В двойственном порядке верхний элемент toDual соответствует нижнему в исходном порядке.

LaTeX

$$$\\\\mathrm{IsTop}(\\\\mathrm{ofDual}(a)) \\\\leftrightarrow \\\\mathrm{IsBot}(a)$$$

Lean4

@[simp]
theorem isTop_ofDual_iff {a : αᵒᵈ} : IsTop (ofDual a) ↔ IsBot a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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