English
Locally finite linear orders admit an IsPredArchimedean instance, hence IsSuccArchimedean by duality.
Русский
Локально конечные линейные порядки обладают инстансом IsPredArchimedean, следовательно IsSuccArchimedean через дуальность.
LaTeX
$$$[LocallyFiniteOrder\\ ι] \\Rightarrow IsPredArchimedean(ι) \\Rightarrow IsSuccArchimedean(ι)$$$
Lean4
instance (priority := 100) [LocallyFiniteOrder ι] [SuccOrder ι] : IsSuccArchimedean ι where
exists_succ_iterate_of_le := by
intro i j hij
rw [le_iff_lt_or_eq] at hij
rcases hij with hij | hij
swap
· refine ⟨0, ?_⟩
simpa only [Function.iterate_zero, id] using hij
by_contra! h
have h_lt : ∀ n, succ^[n] i < j := fun n ↦ by
induction n with
| zero => simpa only [Function.iterate_zero, id] using hij
| succ n hn =>
refine lt_of_le_of_ne ?_ (h _)
rw [Function.iterate_succ', Function.comp_apply]
exact succ_le_of_lt hn
have h_mem : ∀ n, succ^[n] i ∈ Finset.Icc i j := fun n ↦ Finset.mem_Icc.mpr ⟨le_succ_iterate n i, (h_lt n).le⟩
obtain ⟨n, m, hnm, h_eq⟩ : ∃ n m, n < m ∧ succ^[n] i = succ^[m] i :=
by
let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m := Finite.exists_ne_map_eq_of_infinite f
have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm
rcases le_total n m with h_le | h_le
· exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
· exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
have h_max : IsMax (succ^[n] i) := isMax_iterate_succ_of_eq_of_ne h_eq hnm.ne
exact not_le.mpr (h_lt n) (h_max (h_lt n).le)
