feat(set_theory/ordinal/basic): rel_iso.ordinal_type_eq (#14602)

src/set_theory/ordinal/basic.lean

@@ -504,6 +504,10 @@ theorem type_eq {α β} {r : α → α → Prop} {s : β → β → Prop}
   [is_well_order α r] [is_well_order β s] :
   type r = type s ↔ nonempty (r ≃r s) := quotient.eq
 
+theorem _root_.rel_iso.ordinal_type_eq {α β} {r : α → α → Prop} {s : β → β → Prop}
+  [is_well_order α r] [is_well_order β s] (h : r ≃r s) :
+  type r = type s := type_eq.2 ⟨h⟩
+
 @[simp] theorem type_lt (o : ordinal) : type ((<) : o.out.α → o.out.α → Prop) = o :=
 begin
   change type o.out.r = _,