isSuccArchimedean — Mathlib

English

If s is OrdConnected, then s is SuccArchimedean, inherited from PredArchimedean on the dual.

Русский

Если s OrdConnected, то оно SuccArchimedean по наследованию от предикатного архимедова свойства двойственного порядка.

LaTeX

$$$ \forall s:\; s.OrdConnected,\ IsSuccArchimedean(s).$$$

Lean4

instance isSuccArchimedean [SuccOrder α] [IsSuccArchimedean α] (s : Set α) [s.OrdConnected] : IsSuccArchimedean s :=
  letI : IsPredArchimedean sᵒᵈ := inferInstanceAs (IsPredArchimedean (OrderDual.ofDual ⁻¹' s))
  inferInstanceAs (IsSuccArchimedean sᵒᵈᵒᵈ)

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