instIsPredArchimedeanOfLocallyFiniteOrder

Mathlib.Order.SuccPred.LinearLocallyFinite

URI: https://scilib.ai/kg/mathlib#LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder

English

If a locally finite order is given, then IsPredArchimedean holds.

Русский

Если задан локально конечный порядок, то выполняется IsPredArchimedean.

LaTeX

$$$[LocallyFiniteOrder(ι)] \\Rightarrow IsPredArchimedean(ι)$$$

Lean4

instance (priority := 100) [LocallyFiniteOrder ι] [PredOrder ι] : IsPredArchimedean ι :=
  inferInstanceAs (IsPredArchimedean ιᵒᵈᵒᵈ)

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

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

Разделы

Аффилиация

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