instIsSimpleOrder — Mathlib

English

If α is a simple order, then its dual order αᵒᵈ is also a simple order.

Русский

Если α — простой порядок, то его двойственный порядок αᵒᵈ тоже простой порядок.

LaTeX

$$$\text{IsSimpleOrder}(\alpha) \Rightarrow \text{IsSimpleOrder}(\alpha^{\mathrm{op}})$$$

Lean4

instance instIsSimpleOrder {α} [LE α] [BoundedOrder α] [IsSimpleOrder α] : IsSimpleOrder αᵒᵈ :=
  isSimpleOrder_iff_isSimpleOrder_orderDual.1 (by infer_instance)

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