isSimpleOrder_iff_isSimpleOrder_orderDual

English

A simple order remains simple in its dual order: IsSimpleOrder α ⇔ IsSimpleOrder αᵒᵈ.

Русский

Простой порядок сохраняется под двойственным порядком: IsSimpleOrder α ⇔ IsSimpleOrder αᵒᵈ.

LaTeX

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

Lean4

theorem isSimpleOrder_iff_isSimpleOrder_orderDual [LE α] [BoundedOrder α] : IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ :=
  by
  constructor <;> intro i
  · exact { eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
  ·
    exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

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