instLocallyFiniteOrder — Mathlib

English

There is a LocallyFiniteOrder instance on WithBot α obtained via a duality with WithTop αᵒᵈ.

Русский

Существует структура LocallyFiniteOrder на WithBot α, полученная через двойственность с WithTop αᵒᵈ.

LaTeX

$$$ \text{LocallyFiniteOrder}(\mathrm{WithBot}\,\alpha) \cong \mathrm{LocallyFiniteOrder}(\mathrm{WithTop}\,\alpha^{\mathrm{op}}) $$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder (WithBot α) :=
  OrderDual.instLocallyFiniteOrder (α := WithTop αᵒᵈ)

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