toIsPredArchimedean — Mathlib

English

There exists a finite iterate of succ connecting any two comparable elements in a Succ-Archimedean setting.

Русский

Существует конечная итерация succ, связывающая любые два сопоставимых элемента в условиях succ-архимедеева.

LaTeX

$$$ \forall a,b,\exists n, (succ^{[n]} a = b) \lor (succ^{[n]} b = a).$$$

Lean4

instance (priority := 100) toIsPredArchimedean [h : WellFoundedLT α] [PredOrder α] : IsPredArchimedean α :=
  ⟨fun {a b} => by
    refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a) h.wf ?_ b
    intro b ih hab
    replace hab := eq_or_lt_of_le hab
    rcases hab with (rfl | hab)
    · exact ⟨0, rfl⟩
    rcases eq_or_lt_of_le (pred_le b) with hb | hb
    · cases (min_of_le_pred hb.ge).not_lt hab
    dsimp at ih
    obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)
    refine ⟨k + 1, ?_⟩
    rw [iterate_add_apply, iterate_one, hk]⟩

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