isSuccArchimedean_iff_isPredArchimedean

English

In a linear order that is both Succ-archimedean and Pred-archimedean, the two Archimedean notions coincide.

Русский

В линейном порядке, где выполняются и Succ-архимедово, и Pred-архимедово свойства, две концепции Архимедова совпадают.

LaTeX

$$$\\text{IsSuccArchimedean}(\\iota) \\iff \\text{IsPredArchimedean}(\\iota)$$$

Lean4

/-- In a linear `SuccOrder` that's also a `PredOrder`, `IsSuccArchimedean` and `IsPredArchimedean`
are equivalent. -/
theorem isSuccArchimedean_iff_isPredArchimedean : IsSuccArchimedean ι ↔ IsPredArchimedean ι
    where
  mp _ := isPredArchimedean_of_isSuccArchimedean
  mpr _ := isSuccArchimedean_of_isPredArchimedean

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