English
IsSuccArchimedean transfers across order-isomorphisms between SuccOrders.
Русский
Свойство IsSuccArchimedean сохраняется через изоморфизмы порядка между цепями SuccOrder.
LaTeX
$$$ \forall f: X \simeq_o Y,\ IsSuccArchimedean(Y).$$$
Lean4
/-- `IsSuccArchimedean` transfers across equivalences between `SuccOrder`s. -/
protected theorem of_orderIso [SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y] (f : X ≃o Y) : IsSuccArchimedean Y where
exists_succ_iterate_of_le {a b}
h := by
refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
intro n
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
rintro rfl
clear h
induction n generalizing a with
| zero => simp
| succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]
