isBot_ofDual_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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