English
IsPredArchimedean transfers across order-iso between PredOrders.
Русский
IsPredArchimedean сохраняется через ордер-изоморфизм между PredOrder.
LaTeX
$$$ \forall f: X \simeq_o Y,\ IsPredArchimedean(Y).$$$
Lean4
/-- `IsPredArchimedean` transfers across equivalences between `PredOrder`s. -/
protected theorem of_orderIso [PredOrder X] [IsPredArchimedean X] [PredOrder Y] (f : X ≃o Y) : IsPredArchimedean Y where
exists_pred_iterate_of_le {a b}
h := by
refine (exists_pred_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 b with
| zero => simp
| succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]
