isSimpleOrder_iff — Mathlib

English

IsSimpleOrder is preserved by order isomorphisms between bounded orders.

Русский

IsSimpleOrder сохраняется под изоморфизмами порядков между ограниченными порядками.

LaTeX

$$$\forall f:\alpha \simeq_o \beta,\ IsSimpleOrder(\alpha) \iff IsSimpleOrder(\beta)$$$

Lean4

theorem isSimpleOrder_iff [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) : IsSimpleOrder α ↔ IsSimpleOrder β := by
  rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤, f.map_top]

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