toDual_bot — Mathlib

English

In the dual order, the top element maps to the bottom of the original order: ⊤ in the dual corresponds to ⊥ in the original.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toDual_bot [Bot α] : toDual (⊥ : α) = ⊤ :=
  rfl

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