countable_of_linear_succ_pred_arch

English

If ι is a linear order with a successor and predecessor and IsSuccArchimedean, then ι is countable.

Русский

Если множество ι упорядочено линейно и имеет следующие свойства: successor, predecessor и IsSuccArchimedean, то ι счётно.

LaTeX

$$Countable ι$$

Lean4

instance (priority := 100) countable_of_linear_succ_pred_arch : Countable ι :=
  by
  rcases isEmpty_or_nonempty ι with _ | hι
  · infer_instance
  · exact Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv

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