mathlib

f6d2434f - feat(set_theory/cardinal_ordinal): there is no injective function from ordinals to types in the same universe (#9452)

feat(set_theory/cardinal_ordinal): there is no injective function from ordinals to types in the same universe (#9452) Contributed by @rwbarton at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Transfinite.20recursion/near/253614140