dual_dual — Mathlib

English

Dualizing the preorder on α yields the same preorder structure as the original, i.e., the dual preorder is equal to the original preorder.

Русский

Дуализация предорядка на α даёт тот же предорядок, что и исходный.

LaTeX

$$$ \forall \alpha,\; \text{OrderDual.instPreorder}(\alpha^{\mathrm{op}}) = \text{Preorder}(\alpha) $$$

Lean4

theorem dual_dual (α : Type*) [H : Preorder α] : OrderDual.instPreorder αᵒᵈ = H :=
  rfl

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