instIsPredArchimedeanOrderDual

Mathlib.Order.SuccPred.Archimedean

URI: https://scilib.ai/kg/mathlib#instIsPredArchimedeanOrderDual

English

The dual of a PredArchimedean type inherits PredArchimedean properties under the appropriate order dual.

Русский

Дуальная предархимедианность сохраняется при смене порядка на противоположный.

LaTeX

$$$IsPredArchimedean(\text{OrderDual}(\alpha))$$$

Lean4

instance : IsPredArchimedean αᵒᵈ :=
  ⟨fun {a b} h => by convert exists_succ_iterate_of_le h.ofDual⟩

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

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

Разделы

Аффилиация

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