theorem OrderIso.acc_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (a : α) : Acc (fun (x1 x2 : α) => x1 < x2) a ↔ Acc (fun (x1 x2 : β) => x1 < x2) (e a)

theorem OrderIso.acc_iff_symm {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (b : β) : Acc (fun (x1 x2 : β) => x1 < x2) b ↔ Acc (fun (x1 x2 : α) => x1 < x2) (e.symm b)

theorem OrderIso.wellFounded_congr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) : (WellFounded fun (x1 x2 : α) => x1 < x2) ↔ WellFounded fun (x1 x2 : β) => x1 < x2

theorem OrderIso.isWellOrder_congr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) : (IsWellOrder α fun (x1 x2 : α) => x1 < x2) ↔ IsWellOrder β fun (x1 x2 : β) => x1 < x2

theorem OrderIso.wellFoundedLT_congr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) : WellFoundedLT α ↔ WellFoundedLT β

A preorder which embeds into a well-founded preorder is itself well-founded.

theorem OrderIso.wellFoundedGT_congr {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) : WellFoundedGT α ↔ WellFoundedGT β

A preorder which embeds into a preorder in which (· > ·) is well-founded also has (· > ·) well-founded.