toIsSuccArchimedean — Mathlib

English

If α is WellFounded with GT, it is IsSuccArchimedean in the right orientation; archimedean property is transferred via duality.

Русский

Если α хорошо основан (WellFounded) по GT, свойство архимедовости для Succ передаётся через двойственный порядок.

LaTeX

$$$ \text{If } \text{WellFounded}_{GT}(\alpha) \text{ and } \text{SuccOrder}(\alpha), \text{ then } IsSuccArchimedean(\alpha).$$$

Lean4

instance (priority := 100) toIsSuccArchimedean [h : WellFoundedGT α] [SuccOrder α] : IsSuccArchimedean α :=
  let h : IsPredArchimedean αᵒᵈ := by infer_instance
  ⟨h.1⟩

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