English
In a LinearOrder, IsSuccArchimedean and IsPredArchimedean are equivalent; each implies the other when the structure is compatible.
Русский
В линейном порядке эквивалентны свойства IsSuccArchimedean и IsPredArchimedean; одно влечёт другое при совместимости структур.
LaTeX
$$$\\text{IsSuccArchimedean}(\\iota) \\iff \\text{IsPredArchimedean}(\\iota)$$$
Lean4
instance (priority := 100) isPredArchimedean_of_isSuccArchimedean [IsSuccArchimedean ι] : IsPredArchimedean ι where
exists_pred_iterate_of_le {i j}
hij := by
have h_exists := exists_succ_iterate_of_le hij
obtain ⟨n, hn_eq, hn_lt_ne⟩ : ∃ n, succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j :=
⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩
refine ⟨n, ?_⟩
rw [← hn_eq]
cases n with
| zero => simp only [Function.iterate_zero, id]
| succ n =>
rw [pred_succ_iterate_of_not_isMax]
rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
refine lt_of_le_of_ne ?_ ?_
· rw [Function.iterate_succ_apply']
exact le_succ _
· rw [hn_eq]
exact hn_lt_ne _ (Nat.lt_succ_self n)
