isSimpleOrder

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#OrderIso.isSimpleOrder

English

If IsSimpleOrder β and f: α ≃o β, then IsSimpleOrder α.

Русский

Если IsSimpleOrder(β) и f: α ≃o β, тогда IsSimpleOrder(α).

LaTeX

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

Lean4

theorem isSimpleOrder [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) : IsSimpleOrder α :=
  f.isSimpleOrder_iff.mpr h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru