isSuccArchimedean_of_isPredArchimedean

English

A locally finite linear order carries an IsSuccArchimedean instance (hence IsPredArchimedean).

Русский

Локально конечный линейный порядок обладает свойством IsSuccArchimedean (и следовательно IsPredArchimedean).

LaTeX

$$$[LocallyFiniteOrder\\ \\iota] \\Rightarrow IsSuccArchimedean(\\iota) \\Rightarrow IsPredArchimedean(\\iota)$$$

Lean4

instance isSuccArchimedean_of_isPredArchimedean [IsPredArchimedean ι] : IsSuccArchimedean ι :=
  inferInstanceAs (IsSuccArchimedean ιᵒᵈᵒᵈ)

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